LEAP
Free while signed in. Answers cite the passages they came from.
New research from Google shows how far a custom agent harness can push a general-purpose model on formal mathematics. LEAP wraps a general LLM in an agentic scaffold that grounds every step in the Lean compiler and iterates against verifier feedback. Rather than fine-tuning a specialized prover, it leans on informal reasoning, instruction following, and self-refinement, then forces every formal step through a compiler check before moving on.
Decompose, then verify: The scaffold takes the natural form of proof decomposition and verifier-guided refinement. The model breaks a hard theorem into subgoals, drafts an informal blueprint, and the Lean compiler checks each formal step, turning vague reasoning into machine-checkable proof.
Putnam solved in full: On the 2025 Putnam Competition, LEAP solves all 12 problems, matching recent breakthroughs from dedicated frontier math models without any math-specific training of the base LLM.
Large jump on IMO-level proofs: On Lean-IMO-Bench, LEAP lifts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, surpassing the 48% set by a specialized, gold-medal-caliber IMO system.
Why it matters: This is strong evidence that a well-built harness, not a bespoke model, can close the gap on one of the hardest reasoning domains. The leverage sits in the scaffold and the verifier loop around a general model.
Get next week’s papers.
The same picks and the same summaries, in your inbox. Free, and 176 issues deep.
Subscribe on Substack