Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automat

Yep agree. Having an active team of working mathematicians and field medalists giving feedback to the LEAN development team is really helpful in pushing automation forward. Having said that, for people like me, who doesn’t care about formalising mathematics but do care about proving code correct, proof automation has already come a long way and is on the edge of becoming a practical tool for highly critical software.