LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Summary (Overview)

• LEAP (LLM-in-Lean Environment Agentic Prover) is an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving in Lean, without requiring specialized fine-tuning.
• Key innovation: LEAP codifies the human mathematical workflow by combining high-level blueprint sketching (as an AND-OR DAG) with low-level formal proof generation and iterative compiler feedback, demonstrating that general LLMs can outperform specialized prover models when properly scaffolded.
• Benchmark contributions: The paper introduces Lean-IMO-Bench, a curated collection of 60 IMO-style problems formalized in Lean, targeting the regime of elementary statements with highly non-routine, multi-step proofs.
• Empirical results: LEAP solves all 12 problems on Putnam 2025 (100% solve rate), and achieves 83.3% (Basic) / 56.7% (Advanced) on Lean-IMO-Bench, surpassing Aristotle (48% overall) and dramatically improving general LLMs' one-shot performance (from under 10% to 70%).
• Research-level utility: LEAP autonomously formalized a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs, synthesizing over 5,000 lines of Lean 4 code.

Introduction and Theoretical Foundation

Background and Motivation

Large Language Models (LLMs) have demonstrated impressive capabilities in informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. This gap is significant because:

• Natural language proofs suffer from logical fallacies and hallucinations and are hard to verify automatically
• Even for human mathematicians, verifying complex proofs is time-consuming (e.g., the Kepler conjecture required 4 years of peer review and a decade-long formal verification effort)
• Formal mathematics (Lean, Isabelle, Coq, HOL Light) offers automated verification with guaranteed accuracy

The Specialization Assumption

Recent efforts predominantly fine-tune specialized prover models (AlphaProof, DeepSeek Prover V2, Seed Prover, Goedel Prover V2) on formal corpora, operating under the assumption that general LLMs are ineffective for rigorous formal tasks without specialization. According to FormalProofBench and TaoBench, general LLMs often underperform compared to specialized prover models.

Key Insight

The authors challenge this assumption, arguing that:

"While general LLMs remain limited in one-shot theorem proving, the bottleneck is not language comprehension but generating long, complex, correct proofs in one attempt."

General LLMs offer complementary skills to specialized models:

• Strong informal reasoning
• Instruction following
• Tool use
• Self-refinement

These capabilities make them ideal for agentic automated theorem proving (ATP) frameworks, where proof construction is decomposed and iteratively improved.

Methodology

2.1 Blueprint-Driven Formalization

Inspired by the Lean Blueprint tool used in large-scale formalization projects (e.g., Fermat's Last Theorem roadmap), LEAP uses a directed acyclic graph (DAG) where:

• OR nodes represent open goals or lemma statements (any valid proof strategy may resolve them)
• AND nodes represent candidate decompositions whose success depends on proving all constituent subgoals

2.2 LEAP Workflow

The workflow (Figure 1) operates as follows:

1. Direct Proof Attempt: Given an input theorem, LEAP first attempts a direct proof by:

   • Generating an informal proof
   • Translating it into Lean code
   • Checking the candidate with the Lean compiler

2. Decomposition: If direct proving fails, LEAP:

   • Drafts an informal blueprint proposing intermediate lemmas
   • Translates the blueprint into a Lean proof sketch (main theorem body is sorry-free; sorry placeholders only in proposed lemma statements)
   • Adds verified sketches as AND nodes with proposed lemmas as child OR nodes

3. Recursive Processing: The agent recursively processes newly created subgoals, maintaining acyclicity in the DAG.

2.3 Hierarchical Memoization via DAG

The DAG provides two central advantages:

1. Monotone refinement: Once a goal is decomposed, search focuses on descendants without restructuring the established dependency order
2. Lemma memoization: Intermediate lemma statements are stored as shared nodes and reused across branches, supporting anticipatory lemma planning (proposing auxiliary lemmas not immediately required but potentially useful later)

2.4 Interleaved Informal–Formal Planning

Both the direct proof path and decomposition path pass through an informal proof sketch:

• Direct proving: Generate informal argument → translate to Lean candidate proof
• Decomposition: Draft informal blueprint → convert to Lean sketch recording proposed dependencies

This makes proof construction less brittle than direct code generation and makes progress more interpretable.

2.5 Verification-Guided Proof Search

LEAP uses verification at two levels:

1. Lean compiler: Formally checks candidate proofs and sketches (syntactic validity and type-correctness)
2. LLM reviewer: Assesses decomposition quality—whether subgoals are relevant, make the problem easier, and offer a plausible route to completion

The LLM reviewer acts as a search filter that identifies unpromising decompositions, triggers backtracking, and encourages alternative strategies.

Empirical Validation / Results

3.1 Lean-IMO-Bench Dataset

• 60 problems (30 Basic + 30 Advanced), building on IMO-ProofBench
• Balanced across algebra, combinatorics, geometry, and number theory
• Manually formalized and verified by Lean experts

Baseline performance (Table 1):

This demonstrates a stark gap: models can solve problems in natural language but fail at Lean code generation.

4.1 Results on Putnam 2025

Table 2 | Putnam 2025 results (✓ = solved, × = failed; ⋄ = pass@128, † = rollout=2):

Runtime statistics (Table 3): LEAP used 46–3,000 LLM calls per problem, with 8–211 active DAG nodes, producing proofs of 300–2,000 lines.

4.2 Results on Lean-IMO-Bench

Table 4 | Solve rates (%) by category:

5.1 One-Shot vs. Iterative Formalization

Table 5 | Performance on Lean-IMO-Bench Basic set:

Goedel-Prover-V2-32B does not benefit from compiler-feedback revision, while Gemini-3.1-pro improves substantially—demonstrating that iterative formalization requires capabilities beyond local proof synthesis.

5.2 Effect of DAG-Based Memoization

Table 6 | DAG memoization ablation (B = Basic, A = Advanced):

The DAG provides significant improvements, especially on Advanced Algebra and Advanced Number Theory.

5.3 LLM-Guided Proof Search Ablation

On Putnam 2025 Problem A5 (the most challenging case), removing the LLM reviewer causes failure even after 8 rollout attempts. A representative failure mode (Figure 3) shows the agent creating a subgoal syntactically identical to the grandparent goal:

-- Proposed subgoal (syntactically identical to the grandparent goal)
lemma card_perm_s_a_eq_card_perm_s_b
    (m : N) (s : Fin (m + 1) → Z^x) (k : Fin (m + 2)) :
    Nat.card (PermsA m s k) = Nat.card (PermsB m s k) := by sorry

Without semantic review, this duplicate lemma causes the agent to repeat unproductive decompositions until search budget is exhausted.

6. Case Studies: Open Problems

1. Hamiltonian Decomposition of Directed Cayley Graphs: LEAP verified a key subproblem in Knuth's problem—that the 2D planar projection of a single color class's routing dynamics forms an unbroken cycle of length $m^2$—synthesizing over 5,000 lines of Lean 4 code.

2. Erdős Problem 457: LEAP autonomously reconstructed and verified the known proof about triangle-free graph density from first principles.

Theoretical and Practical Implications

Theoretical Implications

1. Challenging the specialization assumption: LEAP demonstrates that state-of-the-art formal theorem proving can be achieved using only general-purpose LLMs, challenging the belief that specialized fine-tuning is indispensable.

2. The bottleneck is interaction, not comprehension: The primary limitation for general LLMs in formal mathematics is not formal language comprehension alone, but the lack of structured, iterative interaction with the proof environment.

3. LLMs as search heuristics: The effectiveness of the LLM reviewer suggests that LLMs may serve as heuristic evaluators for guiding search in formal proof spaces—a broader design pattern beyond theorem proving.

Practical Implications

1. Benchmark saturation: The paper highlights that existing benchmarks (MiniF2F, PutnamBench) are becoming saturated, motivating the introduction of Lean-IMO-Bench for sharper evaluation.

2. Efficiency gains: LEAP's DAG-based memoization mitigates the exponential search complexity of recursive frameworks like Hilbert, which has time complexity $O((n \cdot b)^d)$ where $n$ is lemma retries, $b$ is branching factor, and $d = 10$ is maximum proof depth.

3. Hybrid architectures: While LEAP uses only general LLMs, the authors acknowledge that hybrid designs combining foundation models' structural reasoning with specialized models' focused step generation could be highly effective.

Conclusion

Main Takeaways

• LEAP achieves 100% solve rate on Putnam 2025 and 83.3%/56.7% on Lean-IMO-Bench (Basic/Advanced), surpassing specialized systems like Aristotle (75% Putnam, 48% overall on Lean-IMO-Bench).
• The framework's success rests on three design pillars: DAG-based hierarchical memoization, interleaved informal-formal planning, and verification-guided proof search.
• General-purpose LLMs can progress "from zero to hero" in formal mathematics when properly scaffolded with agentic frameworks.

Future Directions

The central challenge for future work is efficient navigation of proof trees:

• Improving branch prioritization
• Refining decomposition strategies
• Optimizing compute allocation across large proof searches

These advances will be critical for scaling agentic formal proving systems to more complex mathematical problems. The authors also suggest exploring hybrid architectures combining foundation models with specialized provers as a promising design pattern for future research.