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).
One thought on “Formalizations in LEAN”
Comments are closed.