leading formalizers critique rushed AI-driven math formalization push
How to Formalize All of Mathematics (external)
The people who build Lean and Mathlib are telling you that AI-dumped proofs like Claude's 13-million-line Fermat verification carry almost no research value, and they name the vetted channels (Mathlib, Tau Ceti, Formal Frontier, Palomar) where machine-generated formalization is actually worth building on.
- Written collectively by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Remy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz; they explicitly disclaim speaking for any organization. Their core argument: a formal artifact is worthless if nobody uses it, so correctness alone does not justify formalization.
- Cited failures: Math, Inc. tried to hijack a formalization of Viazovska's sphere-packing result, and the original team found cleaning up the AI code more trouble than redoing it; Anthropic's Claude verified Fermat's Last Theorem in 13 million lines over 11 days, which Buzzard calls impressive but of little ongoing value; OpenAI's Navier-Stokes finite-time blow-up shipped with a Lean proof but an 'incomprehensible' write-up, some results since retracted, with informal/formal pairs diverging.
- Cited successes: OpenAI's unit distance conjecture work and Anthropic's Riemann zeta zero density work, which they say contributed understanding and attracted follow-on work.
Full summary
A guest post on the Xena Project blog, co-authored by seven core figures in the Lean and Mathlib formalization community, responds to AI-lab calls to formalize all of mathematics quickly. The authors argue that correctness is not the point: a formal artifact only has value if mathematicians can explore, refactor, and build on it, so bulk AI-generated proofs that nobody uses are a waste or worse. They contrast failures (Math, Inc.'s attempted sphere-packing takeover, Claude's 13-million-line Fermat verification, OpenAI's opaque and partly retracted Navier-Stokes dump) with successes they say advanced understanding (OpenAI's unit distance conjecture, Anthropic's Riemann zeta zero density). They survey the ecosystem they endorse: human-curated Mathlib, the all-AI-written but adversarially reviewed Tau Ceti (~3M lines), the source-to-library pipeline Formal Frontier (41 libraries, ~200k lines), Formal Conjectures, the Annals Challenge, and the Palomar provenance registry. The post lays out shared values (defer to Mathlib, avoid duplication, public review, open publishing, no unaudited code dumps) and claims most of mathematics could be usefully formalized within three years if the work is done well and controlled by mathematicians.