Formalizations in LEAN

I already blogged a few times about computer assisted verification of proofs, for example here: link.

It seems to me that this topic is accelerating fast right now, especially formalizations in LEAN.

• In addition to the example linked above (a verification of a recent result of Clausen-Scholze), an important new result in combinatorics was recently formalized (link to another blog discussing this).
• Kevin Buzzard got a grant for 5-years to formalize a proof of Fermat’s Last Theorem (link). This is extremely ambitious and he himself says that the goal is actually to `only’ formalize the reduction of FLT to a bunch of (major) results from the 1980s.
• And finally, Terence Tao formalized one of his recent papers in LEAN (link).

edit (Nov. 19th): Terence Tao is now also formalizing his recent proof of the Polynomial Freiman-Ruzsa conjecture over F_2: Link.

edit (Nov. 22nd): There are of course also other formal proof assistants besides LEAN. A formalization of the \(\infty\)-categorical Yoneda lemma was recently done in Rzk (arXiv:2309.08340).