LEAP Solves All 12 Putnam 2025 Problems in Lean — General LLMs Beat Specialist Provers With Agentic Framework
A team across Google Cloud AI Research and Google DeepMind published LEAP — LLM-in-Lean Environment Agentic Prover — a paper that changes the argument about what kind of model you need for formal mathematics.
The conventional assumption was that formal theorem proving (writing machine-verified proofs in systems like Lean) requires specialist models fine-tuned on massive formal proof corpora. LEAP uses only Gemini 3.1 Pro — a general-purpose frontier model with no Lean-specific training — and beats every specialist system on two benchmarks.
Putnam 2025: 100%
The 2025 Putnam Competition is the annual undergraduate mathematics contest. In 2025, the top human score was 110 out of 120; the median was 2. Every problem requires multi-step original reasoning.
Benchmark results on Putnam 2025:
| System | Approach | Solve Rate |
|---|---|---|
| LEAP | Agentic (general LLM) | 100% |
| Aristotle | Specialised system | 75% |
| Hilbert | Hybrid agentic | 33% |
| Gemini 3.1 Pro direct | One-shot | 0% |
| Goedel-Prover-V2-32B | Specialised | 0% |
Direct generation with 128 attempts (pass@128) from either a frontier general model or a specialist prover produced zero correct proofs. LEAP, given two rollouts, solved all twelve.
Lean-IMO-Bench: 70% vs Under 10%
The team also introduces a new benchmark: 60 IMO-style problems formalised in Lean by human experts, split into Basic and Advanced sets. Prior approaches collapse on this dataset.
| System | Basic | Advanced | Overall |
|---|---|---|---|
| LEAP | 83.3% | 56.7% | 70% |
| Aristotle | 76.7% | 20.0% | 48% |
| Hilbert | 36.6% | 6.6% | 22% |
| Gemini 3.1 Pro direct | 20.0% | 3.3% | 12% |
| Goedel-Prover-V2 | 10.0% | 0% | 5% |
LEAP achieves 100% solve rate in Algebra and Number Theory across both difficulty tiers. Geometry remains near zero across all systems.
What LEAP Actually Does
The key insight in the paper is that the bottleneck for general LLMs in formal proof is not mathematical reasoning — it is the requirement to write a single large correct proof in one pass. LLMs are good at informal reasoning, planning, and tool use. They are bad at sustaining syntactic correctness across hundreds of proof steps.
LEAP restructures the task. Rather than asking the model to write a complete proof, it:
- Generates a high-level blueprint — an informal proof plan decomposed into subgoals
- Organises subgoals as a DAG — a directed acyclic graph where lemmas are nodes and dependencies are edges
- Proves subgoals iteratively — with Lean compiler feedback after each attempt
- Memoises intermediate lemmas — so the same result is not re-derived in different branches
- Uses an LLM reviewer — to filter unproductive decompositions before they consume budget
This mimics how human mathematicians actually work when facing a hard problem: sketch the argument first, identify the load-bearing lemmas, prove them individually, assemble the result.
The 0% Baseline Is the Headline
The paper spends considerable space on ablations, but the most important number is the simplest: direct one-shot generation, even with 128 attempts, produces nothing on Putnam 2025 and barely anything on Lean-IMO-Bench.
The bottleneck is not model capability — Gemini 3.1 Pro can solve these problems informally. The bottleneck is scaffolding. Give the same model a structured agentic loop with compiler feedback and proof graph memory, and the solve rate goes from 0% to 100%.
This generalises well beyond formal mathematics. It is a data point for a pattern that has been appearing across domains: frontier models constrained to one-shot output underperform the same models embedded in structured agentic pipelines with feedback. The raw intelligence was already there.
Open Source
LEAP’s Lean proofs for all Putnam 2025 problems are available at github.com/google-deepmind/superhuman/tree/main/leap. The Lean-IMO-Bench dataset is at imobench.github.io.