1. Two years ago

In November 2024 I wrote The need for an autoformalizer. Large language models could write mathematics quickly, but their proofs were full of hallucinations and errors. Lean offered the opposite trade: every proof it accepted was correct, but writing one was slow, tedious work. An autoformalizer, a system that translates mathematics written in natural language into Lean and lets the kernel check the result, would join the two. At the end of that essay I described the goal I cared about most: a formalized tree of mathematics, integrating the literature into a single searchable, checkable framework.

At the time this was a speculative position. The best AI systems scored around 2% on FrontierMath [1], and formalizing a single serious theorem was a multi-year human project. Kevin Buzzard had just received a five-year grant of about £934,000 to formalize the proof of Fermat's Last Theorem, and even that project aimed only to reduce the proof to results known in the 1980s [2].

Less than two years later, the situation is unrecognizable. This essay makes two claims. First, autoformalization now works at scale. Second, because it works, we should do the thing I described as the long-term goal in 2024: formalize all known mathematics. In particular, I endorse Jared Duker Lichtman's call for a Mathematics Autoformalization Project [3].

2. An industry formed

The clearest sign that something changed is that people started companies. When I wrote the original essay, the organized efforts in this space were a handful of research teams at large labs, the Lean FRO, and the nonprofit Project Numina. Since then, a whole market has appeared [4].

Organizations in AI for formal mathematics Funding disclosed Undisclosed

    Two trends stand out. First, venture rounds keep growing: Harmonic went from a \$75 million Series A in 2024 to a \$120 million Series C a year later, and Axiom raised a \$200 million Series A in March 2026 [4, 5, 6]. Second, formally verifying mathematics using Lean 4 has gone mainstream. AlphaProof, Aristotle, Gauss, OpenAI's Erdős disproof, and Anthropic's Fermat proof all produce Lean [7, 8].

    3. Autoformalization at scale

    The progress is easiest to see in the size of the largest AI-driven formalizations [9, 10, 11, 12, 13, 14].

    Largest AI-driven Lean formalizations, lines of code (log scale)

    Dotted line: illustrative extrapolation of the average exponential growth between the first and last milestones. Ten billion lines is a hypothetical target for all mathematics; neither the required size nor the completion date is established.

    To see where things currently stand, consider Fermat's Last Theorem. In eleven days in August 2026, an internal Claude model produced a complete Lean proof of it: about 13 million lines outside Mathlib, depending only on Lean's standard axioms, with humans writing nothing but the one-line statement [9]. All of Mathlib, seven years of work by hundreds of mathematicians, is about 2.5 million lines [15].

    But building on top of the FLT development would be difficult. By Anthropic's own account, the code is much longer than it needs to be and not in a form suitable for Mathlib [9]. It proves prerequisites only in the special cases it needs, so the next project cannot simply reuse them, and, as I found in my comparison with its sources, its statements often specialize or repackage the literature rather than translate it.

    Lichtman estimates that all known mathematics would take on the order of 10 billion lines of Lean [3]. A single development of 13 million lines is an achievement; a library that others can extend is something else. Scaling from ten million lines to ten billion will take much stronger infrastructure than we have today.

    4. Mathematics at machine speed

    Mathematics research is evolving. In the past few months we have seen numerous well-known conjectures fall to AI models:

    1. Erdős unit distance conjecture disprovedMay 20, 2026OpenAI [10]
    2. Nine Erdős problems and 44 OEIS conjectures solvedMay 21, 2026DeepMind, AlphaProof Nexus, each with a Lean proof [16]
    3. Jacobian conjecture disproved in three dimensionsJuly 20, 2026Levent Alpöge with Anthropic's Claude Fable 5 [17]
    4. Ten new research resultsAugust 1, 2026OpenAI, backed by about 550,000 lines of Lean [18]
    5. Finite-time blow-up for the forced Navier–Stokes equationsSeptember 8, 2026OpenAI, with a Lean formalization [19]
    6. More than 100 open problems resolvedSeptember 21, 2026OpenAI, as announced with its mathematics advisory group [20]

    Most of these results were found informally and formalized afterward. At its core, mathematics is type theory: every definition introduces a type, every theorem is a type, and every proof is a term of that type. Informal mathematics is an approximation of this. It leaves types implicit, skips steps, and trusts the reader to fill in the gaps. As machines make formal code cheap to write, there will be little reason to work in the approximation, and mathematics will increasingly be done formally from the start.

    Soon machines will produce more mathematics than humans can read, and they can only build on what has been formalized. The unit distance disproof shows the problem. Its new argument is short, but it rests on class field theory, which Mathlib did not contain. A formalization that assumed two results from class field theory took about 33,000 lines [21]; the complete one, assuming nothing beyond Lean's axioms, took 1.2 million [13].

    Thus, every AI result built on modern mathematics faces the same cost: before a machine can check a new theorem, it must formalize the decades of work beneath it. We should pay that cost once, for everyone, by converting all of informal mathematics into formal code.

    5. The next two years

    Formalizing everything will not happen through a series of one-off projects. It needs a coordinated effort and infrastructure that does not exist yet.

    Centralize the effort

    Today, every group formalizes its own prerequisites. The FLT development, the Erdős disproof, and the sphere packing proof each rebuilt background mathematics separately, in forms that do not fit together and mostly never reach Mathlib. The same foundations are paid for again and again.

    Jared Duker Lichtman has proposed the right response: the Mathematics Autoformalization Project (MAP), a coordinated effort to formalize all known mathematics, which he compares to the Human Genome Project [3]. MAP should build one canonical library: each concept defined once, each formal statement linked to the informal result it represents, and each result proved once and reused everywhere. Lichtman calls for coordination among academia, frontier labs, philanthropy, and government. The result should be public, open-source, and independent of any single company, as Mathlib is today.

    Build Lean infrastructure for scale

    Lean's tooling is not yet built for codebases this large. Building the FLT development takes about five and a half hours on a 96-core machine with over 150 GB of memory, and checking it with Lean's comparator takes another 15 hours on a single core with up to 300 GB [9]. Buzzard notes that it takes nearly 20 times as long to compile as all of Mathlib [22], and early users found that builds failed on large cloud machines until they raised an operating system limit on memory mappings [23]. A library of ten billion lines will need what Lean does not yet have: distributed builds, shared caches, parallel checking, and automated maintenance.

    Make the library searchable

    As the amount of formal code grows, finding the right result becomes as hard as proving it. Today's models cannot continually learn, so they will have to navigate the library by searching. This is why I built LeanExplore, which lets agents search Lean declarations by name, code, and informal meaning. But current semantic search struggles with mathematics: a single symbol can change a statement's meaning, while the same theorem can be written in many equivalent forms. Mathlib is 2.5 million lines; the library we envision is orders of magnitude larger. We will need indexing and search algorithms built for mathematical structure and Lean 4.

    6. References

    1. Glazer, Elliot, et al. "FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI," 2024. Link

    2. Buzzard, Kevin. "Fermat's Last Theorem — how it's going." Xena, December 11, 2024. Link; grant EP/Y022904/1, UKRI

    3. Lichtman, Jared Duker. "The MAP: Mathematics Autoformalization Project." X, September 8, 2026. Link

    4. Company funding sources: Harmonic, Axiom, Theorem, Math Inc, Midas, AletheAI, Pramaana Labs, Lanyon AI, Axiomatic AI, DARPA expMath, Atlas Computing, Lean FRO, Mathlib Initiative, Project Numina, XTX Markets

    5. Axiom Math. Series A coverage, SiliconANGLE, March 12, 2026. Link

    6. Harmonic. "Harmonic Builds Momentum Towards Mathematical Superintelligence with \$120 Million Series C," November 25, 2025. Link

    7. DARPA. "expMath: Exponentiating Mathematics." Link

    8. Tao, Terence. "AI for Math Fund." December 5, 2024. Link

    9. Anthropic. "Formalizing Fermat's Last Theorem," September 4, 2026. Link; code at anthropics/fermats-last-theorem

    10. Kalai, Gil. "Amazing: Erdős unit distance problem was disproved." May 21, 2026. Link

    11. Math Inc. "Sphere packing in Lean." Link; code at math-inc/Sphere-Packing-Lean

    12. Math Inc. "Gauss." Link

    13. Buzzard, Kevin. "Human mathematicians are being out-counterexampled." Xena, July 20, 2026. Link

    14. Lean FRO. Announcement of Morph Labs' Trinity autoformalization, June 12, 2025. Link; source paper arXiv:2505.13991

    15. Mathlib community. "Mathlib statistics." Link

    16. Tsoukalas, George, et al. "Advancing Mathematics Research with AI-Driven Formal Proof Search," 2026. Link; results at google-deepmind/alphaproof-nexus-results

    17. Tao, Terence. "A digestion of the Jacobian conjecture counterexample." July 21, 2026. Link

    18. OpenAI. "Ten advances in mathematics," August 2026. Paper; Lean at openai/ten-proofs

    19. OpenAI. Navier–Stokes and Euler blow-up formalization, September 2026. Link

    20. Tao, Terence. "Advisory group on mathematics and artificial intelligence." September 21, 2026. Link

    21. Logical Intelligence. Formalization of the Erdős unit distance disproof. Link

    22. Buzzard, Kevin. "FLT: Anthropic has beaten me to it." Xena, September 4, 2026. Link

    23. Build failures and the memory-mapping limit, anthropics/fermats-last-theorem issue #10. Link