Autoformalization
Translating mathematics that already exists in the literature into a proof assistant's language, by machine. The input is a human proof written for human readers, with its skipped steps and its centuries of assumed background; the output is something Lean's kernel will check line by line.
It is a different activity from proving something new, and cluster E now holds one clean instance of each:
| ten-proofs (OpenAI, 2026-08) | flt-formalization-anthropic (Anthropic, 2026-09) | |
|---|---|---|
| The mathematics | Generated by the model; ten open problems | Wiles 1995, via Darmon–Diamond–Taylor |
| What the Lean adds | A certificate that the new argument is valid | The whole point — nothing else is new |
| What it tests | Reach of the deduction arrow | Whether the translation can be mechanized at scale |
A community effort under kevin-buzzard budgeted years for the FLT formalization, and the blueprint for its first phase alone runs to 86 pages. If eleven days of machine time now does that job, the bottleneck was never the mathematics. It was the labour of restating it.
Why it matters beyond mathematics
Buzzard's stated consequence is the one to watch: autoformalization makes it cheap to check LLM-generated mathematics, which is otherwise "an extremely costly human-led process." That closes a loop the corpus has been circling. lean-certificate argued a formal proof is the rare AI claim a stranger can settle without trusting the claimant; the objection was always that producing the certificate is expensive and only the lab can afford it. Autoformalization at this scale attacks that objection from the other side.
The limits, unchanged
Nothing here touches abduction. Formalizing an existing proof reasons inside an axiom system someone else built, which is the phase llms-cant-jump concedes to machines anyway. And a kernel certifies validity only: not that the theorems matter, not that the statement formalized is the one a mathematician meant — flt-formalization-anthropic answers that last one with a comparator check against Mathlib's own statement of FLT, which is the right instinct and is itself a piece of software someone has to trust.
Scale is not elegance either. Anthropic's proof runs to 13 million lines, over five times Mathlib, and Anthropic says plainly it is "likely much longer than it needs to be."
Related
flt-formalization-anthropic · prove2me · lean-certificate · ten-proofs · lean-theorem-prover · formal-verification · alphaproof · abduction