I attended ItaLean 2025. Alex Best's presentation title "So, Computers Can Prove Theorems (in Lean), What Next?" might as well be the summary of what I'm feeling after the event.

Before and during the event, mathematicians were using autoformalization tools to formalize proofs, definitions and statements. The most frequently mentioned tools at the event were Aristotle and Gauss.

The common understanding was that the tools are advancing quickly. One major theme of the panel discussion was the impacts of autoformalization tools on math education. It was not about whether math education will be impacted, but about what remains important through the upcoming changes. There was even a discussion about the possibility that the role of mathematicians might become similar to that of literary critics.

How and why is this breakthrough happening?

The growing abilities of the autoformalization tools must be one of the biggest factors. Moreover, from what I saw during the event, the culture of the math community is helping a lot. The math community has a way of collaboration that enables mutual respect and productivity, even when a team consists of people with very diverse backgrounds. This has certainly helped formalization projects where most participants are non-experts in the subject matter. Mathematicians' training on rigorous and clear writing is also a big factor that the autoformalization tools and team work can be effective.

Formalization projects are benefitting from the math culture probably because a considerable number of mathematicians have picked up Lean in the first place. For that, the ergonomics of tools must have mattered a lot.

Will this wave of autoformalization spread to program verification?

Certainly, especially where the involved programming languages come with small enough, clear enough and well-tested definitions. One extreme example is Clean, where the programming language consists of polynomial equations (I'm involved).

It was fun

I thank the speakers, the participants and specially the organizers of the event for the insightful week.