Autoformalization

Autoformalization

• Autoformalization means handing mathematics to an agentic LLM, like ChatGPT, Claude or Aristotle (that is free!), and having it produce Lean code on its own.

• Agentic is the operative word: the model writes code, reads what the compiler says about it, and tries again until Lean is happy.

• That loop is why it works. Every attempt gets an honest verdict, and the LLM keeps trying until everything compiles.

• One can use it for a single lemma: hand it over, and ten minutes later it comes back proved, while you get on with something else.

• Nowadays it is also possible to hand over an entire research article and let the LLM work until the formalization is done, sometimes for weeks.

Does it work?

• 20 May, Erdős's unit distance conjecture (1946) is false: a construction found by an OpenAI model. Autoformalized in Lean within a week; unconditionally, in about 1.2 million lines, by 26 June.

• 11 July, Grothendieck's 60-year-old question on finite flat group schemes: a group scheme of order 4 not killed by 4. In Lean four hours later, in a 1076-line file.

• 20 July, the Jacobian conjecture (1939) is false in dimension 3, from a map found by Claude Fable; announced by Levent Alpöge. Paul Lezeau formalizes it the next day. Dimension 2 is still open.

• August, a complex structure on the six-sphere, by Levent Alpöge with Claude, settling a question open since the 1940s; the Lean development follows within days.

Does it work? (continued)

• 20 August, an elliptic curve of rank at least 30, by Claude with Levent Alpöge and Ava Howell, beating a record that had stood at 29 since 2024; rank 31 followed three days later. No Lean needed here: the certificate is thirty explicit independent points.

• 3 September, bounded gaps between primes: H₁ ≤ 212, three days after Julia Stadlmann brought it to 240. AxiomProver generated the Lean certificate of the deduction (conditional on the analytic inputs, not a proof of them). OpenAI separately has H₁ ≤ 186 in Lean, assuming standard Kloosterman bounds.

• 4 September, Fermat's Last Theorem, complete and machine-checked: 13 million lines of Lean, autoformalized in eleven days.

• 8 September, the Kakeya conjecture in dimension 3 (Wang–Zahl, 2025): Project Numina's kakeya-3d formalizes the streamlined Guth–Wang–Zahl argument, and Nankai University with the ByteDance Seed AI4Math Team supply the input it assumes. Linking the two gives KakeyaSetConjecture 3 with no sorry and no axiom beyond Lean's own three. That repository went up the day before this talk.

Navier–Stokes was solved by OpenAI during this very meeting, with a Lean formalization: NavierStokesAndEuler. The statement is taken from the formal conjecture project.

Autoformalized libraries

• We can now have large libraries whose code is written entirely by LLMs, like Tau Ceti, incubated by the Lean FRO and the Mathlib Initiative, with humans owning the roadmap and the review rubrics, and AIs writing and reviewing the mathematics.

• mathlib is still written by humans (sometimes with the help of an LLM) and, above all, it is human reviewed.

• The goals are different. One of the aims of mathlib is to understand the mathematics better, and to organize it in a way that makes sense to a human; an autoformalized library exists to make further autoformalization easier.

Can we really trust a Lean proof?

• Checking correctness is done by Lean's kernel, a very small component that we trust.

• There exist independent external checkers and mathlib is regularly checked against them.

• All of mathlib assumes only (at most...) three axioms:

  1. Propext — basically, a (Prop-valued) function is determined by its values;

  2. Quot — given an equivalence relation on a type, we can construct the quotient type;

  3. Choice — the usual Axiom of Choice.

• Given any project you can ask Lean which axioms it uses, and ask one or more of the checkers to verify that its claim is proven.

• You cannot ask Lean or any of the checkers whether those claims are aligned with your mind.

Can we really trust LLM-written Lean?

• In July a claimed disproof of the Collatz conjecture compiled. It was not a disproof: it exploited a bug in the kernel, and proved False with only the three axioms and no sorry.

• Over the following weeks four more bugs were found in the kernel. All of them are fixed, in Lean v4.33.1.

• Every one of them was reached through heavy, deliberate metaprogramming. Nothing of the kind happens when you are simply writing mathematics.

• So it remains extremely unlikely that a mistake in a human-written proof gets past Lean. That is not what you should worry about.

What's next in autoformalization?

• The classification of finite simple groups is under way.

• So is the Poincaré conjecture.

• There are also libraries of formal statements of open problems, like DeepMind's formal conjectures.

• Every theorem proved by an LLM should come with its formalization.

• That is not the end of the story, of course: it says the result is correct, it does not explain the proof.

So what is the point of learning how to formalize?

• Since Lean checks proofs and not statements, a definition, or the statement of a theorem, can only be checked by a human who knows what it ought to say.

• Autoformalized code is usually hard to read. It tells you that the result is true; it does not teach you the mathematics behind it.

• This is very useful when the mathematics itself was written by an LLM.

• And when you want to be sure of a new result of your own, before you put your name on it.

• It is entirely reasonable to expect that, before long, you will work alongside an LLM that checks your paper in Lean as you write it.