LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

TL;DR

LEAP is a Google agentic framework that turns a general-purpose foundation model into a state-of-the-art Lean theorem prover without specialized training, by bridging informal natural-language reasoning (“blueprints”) with formal proof construction through continuous interaction with the Lean compiler. Complex problems are decomposed into smaller units that the model attempts, verifies, and iteratively refines against compiler feedback. The system solves all 12 problems on Putnam 2025 — matching specialized frontier formal provers — and lifts general-purpose LLMs from <10% to 70% one-shot solve rate on a new Lean-IMO-Bench, surpassing the 48% baseline of a specialized gold-medal-caliber IMO system. LEAP also formalizes a verified proof for a key subproblem in Knuth’s Hamiltonian decomposition conjecture for Cayley graphs.

Key claims

A general-purpose foundation model wrapped in LEAP’s agentic loop matches specialized formal-math frontier systems on Putnam 2025 (12/12 solved) and exceeds a gold-medal-caliber specialized IMO system on Lean-IMO-Bench (70% vs 48% one-shot formal solve rate) [§Abstract].
LEAP raises general-purpose LLM one-shot Lean solve rate on Lean-IMO-Bench from below 10% to 70% — a >7× absolute lift attributed to the agentic scaffold rather than to additional model training [§Abstract].
Decomposing a target theorem into smaller proof units and reconstructing the formal proof through informal blueprints + Lean-compiler feedback is the load-bearing mechanism — the framework leverages informal reasoning, instruction following, and iterative self-refinement as primitives the foundation model already has [§Abstract].
Lean-IMO-Bench is introduced as a saturation-resistant evaluation: short statements but highly non-routine, multi-step IMO-style proofs across a wide difficulty range, designed to push past benchmarks the field is rapidly closing out [§Abstract].
The framework reaches research-level utility by autonomously formalizing a verified proof for a key subproblem in Knuth’s Hamiltonian decomposition of even-order Cayley graphs — i.e. the system contributes a machine-verified result on an open combinatorial problem, not just on competition problems [§Abstract].

Method

LEAP is an agentic scaffold (not a finetuned model) that wires a general-purpose foundation model to the Lean compiler. The model produces an informal natural-language blueprint of the proof, decomposes the target theorem into smaller sub-goals, drafts Lean tactic scripts for each sub-goal, and submits them to the Lean compiler. Compiler errors and unsolved goals feed back into the next iteration, where the model rewrites the failing fragments or revisits the decomposition. The overall loop is “informal blueprint → formal decomposition → compiler check → iterative refinement,” repeated until the proof closes or a budget is exhausted. No new model is trained; the system depends on the foundation model’s instruction-following and reasoning capabilities, with Lean providing ground-truth verification at every step.

Results

Putnam 2025: solves all 12/12 problems, matching recent breakthroughs by specialized frontier formal-mathematics systems [§Abstract].
Lean-IMO-Bench: lifts one-shot formal solve rate of general-purpose LLMs from <10% to 70%; surpasses a specialized, gold-medal-caliber IMO formal system at 48% [§Abstract].
Autonomously produces a Lean-verified proof for a key subproblem in Knuth’s Hamiltonian decomposition conjecture for even-order Cayley graphs [§Abstract].

Why it’s interesting

LEAP is the formal-proof counterpart to DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning: both target IMO/Putnam-grade mathematics, but where DeepSeekMath-V2 trains a 685B model with GRPO against a generator/verifier loop in natural-language proofs, LEAP keeps the base model frozen and gets ground truth from the Lean compiler instead of a learned verifier. The trade-off is clean — DeepSeekMath-V2 pays training compute and risks verifier hallucination (which it patches with a meta-verifier); LEAP pays inference compute and gets a hard correctness signal for free from Lean, at the cost of being tied to what Mathlib already formalizes. The 70% vs 48% headline against a specialized IMO-gold formal system makes the “scaffold-on-a-strong-base-model” bet (Training-Free Group Relative Policy Optimization‘s thesis, Recursive Language Models‘s thesis) land in formal math too. On the Tool-Use Agents axis, Lean is one of the cleanest tools possible — total correctness signal, no observation ambiguity — and the iterative-refinement-against-compiler loop is the structural twin of MiroThinker: Pushing the Performance Boundaries of Open-Source Research Agents via Model, Context, and Interactive Scaling‘s ReAct-against-search-tools loop, just with a verifier instead of an environment. The Knuth-subproblem result also nudges this onto the AI-for-AI Research page’s edge: a fourth granularity where the autonomous loop contributes a machine-verified open-math result rather than a paper or an architecture.