How to Formalize All of Mathematics
A Blueprint for the Formalization of Mathematics
Posted on October 16, 2026, by xenaproject Guest contribution by: Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz.
The mathematical community is currently experiencing a spectrum of emotions—ranging from sheer exhilaration to deep apprehension—following the latest breakthroughs from OpenAI. It has become undeniable that AI has reached a level of proficiency in proving theorems, whether those proofs are presented informally or through formal verification.
Because of these leaps in formal reasoning, some AI proponents are calling for a "grand legacy" project: the immediate formalization of all existing mathematics.
While we admire the potential of these tools to advance the field we love, we feel it is necessary to voice a strong caution. A coordinated, high-quality effort to formalize mathematics could unlock unprecedented discovery; however, a rushed, poorly executed campaign would be a minor setback a catastrophic waste of resources that could inflict permanent damage on the discipline.
The Core Tension
The debate over AI's role in formalization is as polarized as the general debate over AI in mathematics. Even among experts, there is no consensus. Some of our most respected colleagues are fundamentally opposed to using AI for large-scale formalization.
Disclaimer: The views expressed here are those of the authors and do not necessarily represent the organizations or communities they are affiliated with.
The Primary Concerns: Why "Correctness" Isn't Enough
The fundamental premise we hold is that a formal artifact is useless if it is not utilized. We have seen several instances where "impressive" AI feats failed to provide actual mathematical value:
-
The Sphere-Packing Incident: Last February, an attempt was made to use AI to formalize Maryna Viazovska’s work on higher-dimensional sphere-packing. While the AI's capabilities were evident, the result was practically worthless. The human team found that:
- AI generated a massive amount of code.
- The code was riddled with "cruft" and inefficiency.
- Cleaning the AI code was harder than starting over.
- Result: The team discarded the AI code and rebuilt it manually (though still utilizing AI as a tool).
-
Fermat’s Last Theorem: Anthropic claimed that
Claudeverified this theorem using13,000,000lines of code in just 11 days. While Kevin Buzzard acknowledged the feat, he noted that he would continue his own manual formalization of a modern proof. Why? Because the theorem's truth was never in doubt. The value of formalization is not just knowing , but in the process of understanding.
The Value Equation
We believe the value of a formalization can be expressed as:
If , then the remains low, regardless of the correctness.
The Case of the Navier–Stokes Equations
When OpenAI released solutions to the equations that exhibit finite-time blow-up, they provided both a natural-language proof and a Lean formalization. In this specific case, the formalization was vital because the informal proof was nearly impossible for humans to comprehend.
However, this "success" brought its own set of problems:
- Provenance: Questions arose regarding how the result was derived.
- Credit: Concerns over who deserves the intellectual credit.
- Philosophy: A fear that prioritizing "correctness" over "insight" undermines the spirit of the Millennium Prize.
| Approach | Focus | Outcome | Risk |
|---|---|---|---|
| Traditional | Understanding | Insight & Elegance | Human Error |
| AI-Driven (Fast) | Verification | Correctness Signal | "Black Box" Mathematics |
| Hybrid (Ideal) | Synthesis | Verified Insight | High Resource Demand |
OpenAI's subsequent data dumps have been a mixed bag: they contain brilliant mathematics but show a blatant disregard for the reader. Many informal write-ups are impenetrable, and some results have even been retracted.
The Risks of a "Grand Failure"
If we spend millions of dollars creating libraries of formal proofs that no human can navigate or use, we aren't just wasting money. We risk:
- Disincentivizing rigorous, human-led research.
- Destroying the social norms of mathematical collaboration.
- Setting the field back by decades.
A low-quality formalization is worse than no formalization at all.
A Path Forward: The Positives
It is not all bleak. Some efforts have been exemplary. Specifically:
- OpenAI's work on the unit distance conjecture.
- Anthropic's research on the density of Riemann zeta zeroes.
These projects succeeded because they didn't just "solve" a problem; they contributed to the community's understanding and provided a foundation for others to build upon. We welcome more partnerships of this nature.
Contributors & Community:
