LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

• Natural-language mathematical reasoning is strong, but formal provers lag behind general-purpose LLMs, while prior agentic systems still rely on specialized models for Lean proving.Source: §1 · pp. 1–2
• LEAP uses general-purpose LLMs to build a blueprint DAG, generate Lean proofs, and iteratively correct errors using compiler feedback.The authors identify generating long, complex, correct proofs in one attempt—not language comprehension—as the one-shot bottleneck.Source: §1 · p. 2
• Lean-IMO-Bench formalizes IMO-Bench problems in Lean to test short statements whose solutions require non-routine insights and long, structurally intricate proofs.Source: §1 · p. 2
• LEAP solves all 12 Putnam 2025 problems in Lean and reaches 70% on Lean-IMO-Bench, versus below 10% for general LLMs, 5% for specialized ATP models, and 48% for Aristotle.Source: §1 · p. 2

2.1. Formalizing Proofs with Blueprints

• LEAP incrementally drafts blueprints, decomposes Lean goals into supporting lemmas, and maintains the plan as an AND-OR DAG rather than synthesizing a full proof in one pass.Source: §2.1 · p. 3

2.2. Overview

• For each open goal, LEAP tries a direct proof first; if that fails, it compiles a blueprint-derived sketch with proposed lemmas as subgoals and adds the decomposition only if acyclicity is preserved.The sketch has no sorry placeholders in the main theorem body; placeholders are allowed only in proposed lemma statements.Source: Figure 1 · p. 3, §2.2 · p. 4

2.3. Hierarchical Memoization via DAG

• The DAG preserves dependency structure while allowing local proof attempts to change, and stores shared or anticipatory lemmas for reuse across branches.Its visible state also exposes open goals, resolved lemmas, and nodes blocking downstream progress.Source: §2.3 · p. 4

2.4. Interleaved Informal–Formal Planning

• LEAP pairs informal arguments or blueprints with Lean proofs or sketches, giving the model a planning space and users an inspectable rationale for formal steps.Source: §2.4 · p. 5

2.5. Verification-Guided Proof Search

• The Lean compiler checks proof validity, while an LLM reviewer filters decompositions for relevance and tractability, triggering backtracking from weak branches.LEAP currently uses depth-first search over the DAG with backtracking.Source: §2.5 · p. 5

3.1. Lean-IMO-Bench

• Lean-IMO-Bench contains 60 problems split evenly between Basic and Advanced sets, with 30 problems in each.Source: §3.1 · p. 6
• The Basic set spans pre-IMO to IMO-Medium difficulty and includes algebra, combinatorics, number theory, and geometry problems.Its subject counts are 8, 8, 8, and 6, respectively.Source: §3.1 · p. 6
• The Advanced set includes novel problems up to IMO-Hard difficulty and covers algebra, combinatorics, number theory, and geometry.Its subject counts are 8, 8, 6, and 8, respectively.Source: §3.1 · p. 6
• Lean experts manually formalized and verified all 60 statements; the problems require elementary mathematical background, and their solutions are expected to be concise.The dataset design removes overhead from formalizing complex, modern mathematical theories.Source: §3.1 · p. 6
• The benchmark supports Natural Language Proof, Formal Theorem Proving, and Formal Proof Translation, while this paper focuses on formal theorem proving.Table 1 summarizes baseline performance across these tasks; Natural Language Proof performance is based on human expert review.Source: §3.1 · p. 6, Table 1 · p. 6
• Strong natural-language proof performance does not directly translate to Formal Theorem Proving, especially on Advanced problems; proof translation yields unchanged Pass@128 and only a marginal Average@128 gain.Source: §3.1 · p. 6
• The baseline gap indicates that reliably generating valid Lean code remains the primary challenge even when models can solve the problems in natural language.Source: §3.1 · p. 6

4. Experimental Results

• Evaluation used Gemini-3.1-pro as LEAP’s backend and compared it with direct generation, specialized and agentic proving systems on Putnam 2025 and Lean-IMO-Bench.Lean-IMO-Bench provides a complementary test across mathematical disciplines and complexity tiers.Source: §4 · pp. 6–7, §4.2 · p. 7

4.1. Results on Putnam 2025

• On Putnam 2025, direct formalization baselines solved no problems under Pass@128; Hilbert solved 4/12 and Aristotle solved 9/12 with two rollouts.Hilbert’s recursive search led to redundant LLM calls and a seven-day rollout limit.Source: §4.1 · p. 7
• 12/12 Putnam 2025 problems were solved by LEAP, raising the solve rate from 0% for direct formalization to 100%.Table 2 presents the Putnam results.Source: §4.1 · p. 7, Table 2 · p. 7

4.2. Results on Lean-IMO-Bench

• Across evaluated methods, Geometry performance remained near zero, while several systems degraded sharply on the Advanced set.The benchmark retains Geometry to test general-purpose reasoning under extreme formalization constraints.Source: §4.2 · p. 8
• 83.3% on the Basic set and 56.7% on the Advanced set were LEAP’s highest overall solve rates on Lean-IMO-Bench.LEAP also maintained a 100% solve rate in Algebra and Number Theory across both difficulty tiers.Source: §4.2 · p. 8, Table 4 · p. 8

5.1. Beyond One-Shot Formalization

• Gemini-3.1-pro improves from 20.0% one-shot Pass@128 to 36.6% iterative Pass@1, while Goedel-Prover-V2-32B does not benefit from feedback.The iterative setting allows one initial attempt and up to 20 compiler-feedback revisions.Source: §5.1 · p. 9, Table 5 · p. 9
• Compiler-error interpretation, context maintenance, and multi-step revision can matter as much as one-shot proof accuracy for iterative formalization.The authors leave open combining a general foundation model’s reasoning backbone with specialized provers for local proof generation.Source: §5.1 · p. 9

5.2. Effect of DAG-Based Memoization

• 83.3% on Basic and 56.7% on Advanced, versus 73.3% and 40.0% for the tree variant, show gains from DAG-based proof memory.The tree variant already outperforms Hilbert, which scores 36.6% on Basic and 6.6% on Advanced.Source: §5.2 · p. 9, Table 6 · p. 9
• DAG memory supports anticipatory lemma reuse and sharing repeated subproblems, reducing redundant derivations and improving proof-search efficiency.The reported improvement is especially pronounced in Advanced Algebra and Advanced Number Theory.Source: §5.2 · p. 9

5.3. Toward LLM-Guided Proof Search

• On Putnam 2025 Problem A5, removing the decomposition reviewer causes failure after eight rollouts, while LEAP succeeds in two.Without semantic review, an admissible decomposition repeats a subgoal equivalent to the original goal until the search budget is exhausted.Source: §5.3 · p. 10, Figure 3 · p. 10

5.4. Perspective: General LLMs as Formal Provers: From Zero to Hero

• The discussion argues that general foundation models can handle complex formal problems when an agentic workflow scaffolds their reasoning and self-correction.The paper’s primary goal is to demonstrate standalone general-purpose LLMs; a hybrid with specialized models for local proof generation remains outside scope.Source: §5.4 · pp. 10–11

Hamiltonian Decomposition of Directed Cayley Graphs

• LEAP verified the cycle-merging dynamics in Knuth’s even-order Cayley-graph construction, producing over 5,000 lines of Lean 4 code for a critical subproblem.The formalized subproblem verifies that one color class’s 2D routing projection forms an unbroken cycle of length m^2; the informal argument spans roughly 20 pages.Source: §6 · p. 11
• The target problem asks whether the directed arcs of the graph can be partitioned into three distinct spanning Hamiltonian cycles.The informal even-case construction uses combinatorial analysis and localized defect routing across graph layers.Source: §6 · p. 11

Formalizing Erdős Problem 457

• LEAP reconstructed and verified the established proof of Erdős Problem 457 from first principles in Lean 4, without human intervention.The problem concerns the density of triangle-free graphs.Source: §6 · p. 11

• General-purpose LLMs can support rigorous domain-specific reasoning when coupled with appropriate structural scaffolding.For formal mathematics, the paper identifies proof decomposition and verifier-guided refinement as that scaffolding.Source: §7 · p. 11
• LEAP decomposes complex theorems into smaller subgoals and uses Lean to check each formal step, structuring the translation from informal reasoning to verified proofs.Source: §7 · p. 11
• As decomposition creates finer-grained subgoals, the search space can grow rapidly; future systems should improve branch prioritization, decomposition, and compute allocation.The conclusion identifies these advances as important for scaling agentic proving to more complex problems.Source: §7 · p. 11

• LeanDojo and MiniF2F support generative Lean proving through libraries, interactive step-level search, and difficulty evaluation.HyperTree Proof Search and related Monte Carlo tree-search methods explore tactic-level search.Source: A. Related Work · p. 16
• Whole-proof generation and informal blueprints offer alternatives to tactic-level search; LEAP uses general LLMs to draft blueprints and refine proofs through compiler feedback [First et al., 2023; Xin et al., 2025a; Jiang et al., 2023].The passage distinguishes LEAP by not relying on specialized fine-tuned models for formalization.Source: A. Related Work · p. 16
• Specialized models such as AlphaProof scale training and search on formal systems but require substantial training resources and specialize in particular languages.The related-work discussion contrasts them with LEAP’s general-purpose models in an agentic environment.Source: A. Related Work · p. 16
• LEAP uses general LLM auto-formalization capabilities to connect informal blueprints with formal proofs, addressing the gap between strong natural-language math and low formal solve rates.The passage describes auto-formalization pipelines as also being used to generate formal statements for prover training at scale.Source: A. Related Work · p. 16

Hamiltonian Decomposition of Directed Cayley Graphs

• For the even-case Cayley-graph construction, the Color 2 round map must return every point after (2h)^2 steps and have no shorter positive return.The graph is projected onto a 2D grid, and the formal statement encodes the map’s structural defects, coordinate shifts, and piecewise transitions.Source: B. Problem Statements · pp. 17–18

Erdős Problem 457

• Erdős Problem 457 asserts that some ε > 0 makes every prime p ≤ (2 + ε) log n divide the product of ⌊log n⌋ consecutive integers after n, for infinitely many n.The product runs over integers n + 1 through n + ⌊log n⌋.Source: B. Problem Statements · p. 18

Formal context

• A proof sketch proves the current Lean goal while assuming proposed lemmas; its sorry placeholders are restricted to those lemmas, which must later be proved.Once the referenced lemmas are proved, the verified sketch establishes the current goal.Source: C. Proof Contexts and Artifacts · p. 19

Example Proof Goal (Lean-IMO-Bench, Basic 001)

• The Basic 001 example states a functional equation over integer-valued functions and targets the classification as zero or x ↦ 2x + c.The displayed Lean goal is the set equality between functions satisfying the equation and that classified set.Source: C. Proof Contexts and Artifacts · p. 19

Informal context

• An informal proof is a natural-language plan for proving a goal directly, while an informal blueprint reduces it to supporting lemmas that become formal subgoals in the proof DAG.The blueprint may include auxiliary lemmas intended for later proof steps.Source: C. Proof Contexts and Artifacts · p. 21

Example Informal Proof (Lean-IMO-Bench, Basic 001)

• The informal Basic 001 proof derives additivity after shifting f by f(0), then concludes f(x) = kx + c and restricts k to 0 or 2.The resulting cases are the zero function and functions of the form x ↦ 2x + c.Source: C. Proof Contexts and Artifacts · p. 22

Example Informal Blueprint (Lean-IMO-Bench, Basic 006)

• The Basic 006 blueprint bounds the polynomial degree parameter k by K(c) using root-based multisets, Vieta’s formulas, and AM-GM.It constructs products excluding each root and uses a nonzero integer product to obtain the AM-GM bound.Source: C. Proof Contexts and Artifacts · p. 23

Example Formal Proof (Lean-IMO-Bench, Basic 001)

• The Basic 001 formal proof example organizes the polynomial argument into lemmas for coefficient extraction, root counts, multiset identities, and an AM-GM bound.The blueprint’s steps are translated into Lean operations on polynomial roots and multisets before deriving k ≤ K(c).Source: C. Proof Contexts and Artifacts · pp. 23–24