AI for Formal Mathematics

Mathematics is the rare domain with a perfect verifier. A proof written in Lean or Coq either type-checks or it does not, and the checker is a small, auditable program. That removes the problem that limits every other application of language models: you cannot be fooled by a fluent wrong answer, because the kernel does not read prose.

This makes formal mathematics the cleanest possible setting for reinforcement learning from verifiable rewards, and the results reflect it.

Two systems, two architectures

AlphaGeometry pairs a language model with a symbolic deduction engine. The symbolic engine derives everything that follows from the current diagram by forward chaining; when it stalls, the neural model proposes an auxiliary construction, such as a new point or line, which reopens the deduction. Trained on 100 million synthetic theorems generated by random construction plus deduction, with no human proofs, it solved 25 of 30 olympiad-level geometry problems, against 25.9 for an average IMO gold medallist (Trinh et al., Nature, 2024, Solving olympiad geometry without human demonstrations).

The division of labour is the lesson. Search over auxiliary constructions is enormous and unstructured, which suits a learned proposal distribution; deduction from a fixed set of rules is mechanical, which suits a symbolic engine. Neither half solves the problem alone.

AlphaProof works in Lean across general mathematics. It formalises the problem statement, then runs an AlphaZero-style loop: a network proposes proof steps, tree search explores them, and the Lean kernel provides the reward. Because the reward is machine-checkable, the loop can generate its own curriculum, including proving variants and negations of a statement it cannot yet settle. At IMO 2024, AlphaProof solved three of the five non-geometry problems and, together with AlphaGeometry 2, reached 28 of 42 points, a silver-medal score one point below the gold threshold (DeepMind, 2024; published as Olympiad-level formal mathematical reasoning with reinforcement learning, Nature, 2025).

Two caveats that DeepMind stated and reporting often dropped: the problems were manually formalised into Lean, and the system took up to three days on some problems against the competition's 4.5 hours.

The autoformalisation bottleneck

That first caveat is the field's central open problem. A verifiable reward exists only once a statement is formal, and translating natural-language mathematics into Lean is itself hard, unverifiable, and where errors hide. A subtly mis-formalised statement can be proved correctly and mean nothing, and the kernel cannot detect this because the kernel never sees the original.

Compounding it, formal corpora are tiny. Lean's mathlib is large by formal-mathematics standards and vanishing next to any pretraining corpus, so the data that would teach a model to formalise well barely exists. Most progress has come from generating synthetic formal statements and from expert iteration, where a model's own verified proofs are fed back as training data.

Why the verifier changes the economics

With a checker in the loop, generate-and-test becomes viable at scale: sample thousands of candidate proofs, keep the ones that compile, train on those. There is no reward model to hack, no judge to persuade, no contamination question about whether the answer was memorised, because a memorised proof that does not type-check scores zero.

This is the same structure as RLVR in code and maths generally, in its purest form. It also explains why formal mathematics advances faster than informal mathematics on benchmarks while contributing less, so far, to mathematics as practised.

When it breaks

Competition problems are a narrow target. IMO problems are hard, self-contained, and known to have short solutions. Research mathematics is open-ended, definition-heavy, and often about finding the right statement rather than proving a given one.

Compute per problem is enormous and rarely reported alongside the headline. Days of search for one olympiad problem is not a tool a mathematician can use interactively, and the gap between benchmark feasibility and practical utility is mostly this.

The verifier verifies the formal statement only. Everything upstream, the formalisation, the choice of definitions, the assumption that the formal statement captures the informal one, is unverified and human-dependent.

Search does not explain. A machine-found proof that type-checks may be long, unmotivated, and mathematically uninteresting. Verification answers "is it true"; mathematicians mostly want "why", and no current system optimises for that.