# LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

arXiv: https://arxiv.org/abs/2606.03303 · HTML: https://mlsanity.com/paper/2606.03303/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 26 of its 38 references that are in the map.
- First posted on arXiv 2 Jun 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)
- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 26 of 26)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Semi-Autonomous Mathematics Discovery with Gemini: A Case Study on the ErdHos Problems](https://mlsanity.com/paper/2601.22401/) (2026)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?](https://mlsanity.com/paper/2603.12744/) (2026)
- [FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?](https://mlsanity.com/paper/2603.26996/) (2026)
- [Metamath Zero: The Cartesian Theorem Prover](https://mlsanity.com/paper/1910.10703/) (2019)

## Built on by (most cited first, 12 of 12)

- [Recursive Self-Improvement in AI: From Bounded Self-Refinement to Autonomous Research Loops](https://mlsanity.com/paper/2607.07663/) (2026)
- [AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis](https://mlsanity.com/paper/2607.03656/) (2026)
- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)
- [Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution](https://mlsanity.com/paper/2607.17352/) (2026)
- [MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4](https://mlsanity.com/paper/2608.02295/) (2026)
- [SkillSpec: Intent-Masked Specification Reasoning for Agent Skill Correctness](https://mlsanity.com/paper/2609.06052/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Thinking Outside the Box: Can Language Models Rely on External Guidance Selectively?](https://mlsanity.com/paper/2609.39578/) (2026)
- [LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs](https://mlsanity.com/paper/2610.11862/) (2026)
- [Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify](https://mlsanity.com/paper/2610.13632/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.