Learn · Intermediate

Autoformalization: turning a written proof into one a machine can check

Autoformalization is the automatic translation of ordinary mathematical writing into a formal language that a computer can verify. A mathematician writes "clearly, by compactness, the sequence admits a convergent subsequence"; an autoformalization system turns that into explicit code in a language like Lean, where the word "clearly" is not allowed and every appeal to compactness must name the theorem it is invoking. It matters because it is the step that converts an argument you have to trust into an argument you can check.

To see why this is a distinct problem, separate two things that often get merged. A proof assistant is software — Lean, Coq, Isabelle — that reads a proof written in its formal language and mechanically confirms every inference against the axioms. That part is essentially solved and has been for decades. The bottleneck was always the input. Formalizing a research-level theorem by hand was a notorious slog: the Kepler conjecture took a team over a decade, and a routine graduate-textbook result could eat a week. Proof assistants were trustworthy and almost nobody used them, because the price of admission was too high.

Autoformalization attacks that price. The insight, developed in work like Google's Autoformalization with Large Language Models, is that translating mathematics into Lean looks a great deal like translating English into French — and language models are good at translation. Feed a model informal statements paired with their formal versions and it learns the mapping. The 2022 result that made people pay attention was that a large model, given no task-specific training at all, could correctly formalize a meaningful fraction of competition mathematics problems just from a handful of examples.

There is a wrinkle that makes this harder than ordinary translation, and it is worth understanding because it shapes how these systems are built. In French translation, a slightly clumsy sentence is still comprehensible. In Lean, a proof that is 99% correct does not compile. It fails, completely, with an error message. There is no partial credit.

That brittleness turns out to be the feature. Because the compiler gives an unambiguous verdict, a system can generate a candidate formalization, get told exactly where it broke, and try again — a loop that needs no human judgement and no labelled data. This is why theorem proving became such a productive testbed for AI reasoning: it is one of the few domains offering a perfect, free, automatic reward signal. That is the same property that makes reinforcement learning with verifiable rewards work, and formal mathematics is its cleanest possible instance. OpenAI's Formal Mathematics Statement Curriculum Learning and later open efforts such as DeepSeek-Prover both lean on exactly this: generate, compile, learn from the failures, repeat, at enormous scale.

The most practically important design pattern is the one introduced in Draft, Sketch, and Prove, and it mirrors how mathematicians actually work. Rather than asking a model to emit a complete formal proof in one shot, you let it first draft an informal argument in ordinary prose, where its fluency is an asset. That draft is then converted into a formal sketch — the skeleton of the argument with the hard steps left as stated-but-unproven gaps. Finally, an automated prover is turned loose on each gap individually. The division of labour is the point: the language model supplies strategy, which is what it is good at, and mechanical search supplies the tedious steps, which is what it is bad at. A human mathematician does the same thing when they say "the idea is to induct on n, and then the base case is routine" — the idea is the contribution, the routine part is delegated.

Why this matters right now: autoformalization has moved from a research curiosity to infrastructure fast enough that experts remark on it. When AI systems began producing claimed proofs of significant results, the field's immediate response was not to read the PDF but to ask for the Lean file — because a language model producing fluent, authoritative, subtly wrong mathematics is simply hallucination in a suit. Machine-checkable output turns an unfalsifiable claim into a falsifiable one. Terence Tao, reviewing recent AI-assisted proofs of finite-time blowup in fluid equations, noted almost in passing that formalizing them in Lean is now "remarkably feasible in the modern era of autoformalization agents." A capability that was a multi-year project is now something that happens in the same week as the result.

The limit is real and easy to overlook. Autoformalization guarantees that a proof of the formal statement is valid. It does not guarantee that the formal statement is the theorem anyone cared about. Misstate a hypothesis — drop a quantifier, weaken a condition, formalize a special case — and the machine will cheerfully certify an airtight proof of something trivial or irrelevant. So human judgement does not disappear; it relocates. Instead of checking a thousand steps, an expert checks one thing very carefully: that the formal statement at the top of the file says what the English sentence says. That is a much better division of labour, and it is also the place where the next generation of errors will hide.

Ground Truth. (2026, September 8). Autoformalization: turning a written proof into one a machine can check. Ground Truth. https://groundtruth.day/learn/autoformalization.html

@misc{groundtruth:autoformalization,
  title  = {Autoformalization: turning a written proof into one a machine can check},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/learn/autoformalization.html}
}

Topics: formal-verification · reasoning · math · lean · evaluation · ai-for-science