LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
LEAP uses blueprint-driven decomposition and iterative self-correction to boost formal proof success from below 10% to 70%, solving all 12 Putnam 2025 problems.
Key Findings
Methodology
LEAP integrates large-scale pre-trained models' informal reasoning with a hierarchical proof planning approach. It generates high-level blueprints—directed acyclic graphs (DAG)—that decompose complex theorems into manageable subgoals. The system iteratively refines proofs by translating informal blueprints into formal Lean code, then verifies correctness via compiler feedback. This process involves three core components: blueprint generation, formal proof synthesis, and feedback-guided revision. By leveraging LLMs' instruction-following and reasoning capabilities, LEAP bridges informal strategies with formal verification, enabling multi-step proofs that outperform previous methods in success rate and efficiency.
Key Results
- On the 2025 Putnam competition, LEAP achieved a 100% solve rate across all 12 problems, a significant improvement over baseline models' 0%.
- On Lean-IMO-Bench, LEAP raised the one-shot formal proof success rate from under 10% to 70%, surpassing the 48% of specialized ATP systems.
- LEAP autonomously formalized complex proofs, including a verified subproof in Knuth’s Hamiltonian decomposition, demonstrating research-level applicability.
Significance
This work addresses the longstanding challenge of automating formal mathematical proofs using general-purpose models. By combining hierarchical blueprints, iterative feedback, and formal verification, LEAP demonstrates that large models can reliably produce machine-checkable proofs, transforming AI-assisted mathematics. It bridges the gap between natural language reasoning and rigorous formalization, opening new avenues for automated theorem proving, mathematical research, and educational tools. The approach also suggests that structured interaction and self-correction are key to scaling AI's capabilities in complex logical tasks, impacting both academia and industry.
Technical Contribution
The primary innovation is the integration of hierarchical blueprint planning with verification-guided self-correction within a DAG structure, enabling reuse of intermediate lemmas and transparent proof management. Unlike prior approaches relying on specialized models, LEAP solely employs general LLMs, demonstrating their sufficiency for high-level formal reasoning. The system's design allows continuous interaction, refinement, and decomposition, significantly improving success rates and efficiency. This architecture provides a new paradigm for AI-driven formal proof synthesis, combining natural language reasoning with formal verification in a unified framework.
Novelty
LEAP is the first framework to fully utilize general-purpose LLMs for hierarchical, blueprint-based formal theorem proving with iterative feedback. It departs from traditional single-pass or purely specialized models, introducing a DAG-based proof decomposition and reuse mechanism that dramatically enhances success rates. Its combination of informal reasoning, formal verification, and self-refinement in an integrated agentic system marks a significant step forward in AI mathematics automation.
Limitations
- LEAP's performance diminishes in highly abstract or geometric domains lacking explicit domain knowledge, indicating the need for domain-specific enhancements.
- The approach involves extensive LLM calls, leading to high computational costs and scalability challenges.
- BluePrint generation may sometimes produce suboptimal decompositions, requiring further improvements in planning strategies.
Future Work
Future directions include integrating domain-specific knowledge bases to improve performance in specialized fields like geometry, optimizing the blueprints for efficiency, and reducing computational costs. Additionally, expanding multi-modal inputs, such as diagrams or symbolic data, could broaden applicability. Developing more intelligent blueprints and incorporating human-in-the-loop strategies may further enhance robustness and interpretability, paving the way for broader deployment in mathematical research, education, and industrial verification tasks.
AI Executive Summary
LEAP (LLM-in-Lean Environment Agentic Prover) represents a groundbreaking advancement in automated formal mathematics. Traditional large language models excel at informal reasoning but struggle with generating verifiable Lean proofs, especially for complex, multi-step theorems. LEAP addresses this challenge by adopting a hierarchical, blueprint-driven framework that decomposes proofs into manageable subgoals, managed within a directed acyclic graph (DAG). This structure enables the system to iteratively generate, verify, and refine proofs through continuous interaction with the Lean compiler, leveraging the reasoning strengths of general-purpose LLMs.
The core innovation lies in combining informal reasoning, high-level blueprint planning, and formal verification into an integrated loop. When faced with difficult goals, LEAP first attempts direct formalization. If unsuccessful, it drafts an informal blueprint, proposing intermediate lemmas and decompositions. These blueprints are then translated into Lean code, verified, and refined based on compiler feedback. This iterative process ensures correctness and efficiency, significantly boosting proof success rates.
Empirical results demonstrate LEAP’s remarkable capabilities: it solves all 12 problems in the 2025 Putnam competition, achieving a 100% success rate, and raises the formal proof success rate on Lean-IMO-Bench from below 10% to 70%. Moreover, LEAP autonomously formalized complex proofs, including a key subproblem in Knuth’s Hamiltonian decomposition, showcasing its research-level utility. These breakthroughs highlight the potential of general LLMs in automating high-level mathematical reasoning, challenging the notion that only specialized models can handle formal proofs.
The significance of this work extends beyond mathematics. It paves the way for AI systems capable of rigorous verification in scientific research, engineering, and education. By demonstrating that structured, interactive workflows can unlock the full potential of large models, LEAP sets a new standard for AI-driven formal reasoning. Future work will focus on domain adaptation, efficiency improvements, and multi-modal reasoning to further expand its impact.
Deep Dive
Plain Language Accessible to non-experts
想象你在厨房里准备一道复杂的菜肴。你不会一下子就把所有材料和步骤都记得清清楚楚，而是会先画一张菜谱，写出大致的做法，比如先炒菜、再调味，然后逐步细化每个步骤，确保每个环节都正确。每次遇到难题时，你会试着做一部分，尝试后发现不行，就重新调整菜谱，直到菜肴完成。LEAP就像这个聪明的厨师，它会先画出一份详细的菜谱（蓝图），告诉自己每一步怎么做，然后一步步去做、检查、修正，直到做出一道完美的菜。这种方法让复杂的菜肴变得更容易做，也更快成功。它用类似的方式，把复杂的数学证明拆成简单的部分，一步步验证，最后拼出完整的答案。
ELI14 Explained like you're 14
想象你在玩一个超级难的拼图游戏。你不知道怎么拼，但你会先画一张草图，标出大致的拼法。然后你试着拼一部分，发现不对，就重新调整。你还会记住之前拼好的部分，下次遇到类似的拼法就可以直接用。这就像LEAP一样，它会先画出一份蓝图，告诉自己怎么一步步拼出数学证明。遇到难题时，它会试着写出部分证明，然后不断检查，直到拼出完整的答案。这让拼图变得更容易，也更快完成。
Abstract
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.