LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Two agentic frameworks, LEAP and Goedel-Architect, have made significant advancements in formal theorem proving using the Lean formal language.
LEAP, described in a paper on arXiv[1], enables large language models to generate mechanically verifiable proofs in formal languages like Lean. It achieves this by leveraging foundation model capabilities such as informal reasoning and iterative self-refinement. LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70% on the Lean-IMO-Bench, surpassing the 48% benchmark set by a specialized IMO system[1]. Meanwhile, Goedel-Architect, detailed in another arXiv paper[2], streamlines formal theorem proving in Lean 4 with blueprint generation and refinement. It uses a dependency graph to build up to the main theorem and attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench[2]. Both frameworks have demonstrated their capabilities on prestigious mathematical competitions. LEAP solved all 12 problems on the 2025 Putnam Competition, while Goedel-Architect solved 11 out of 12 problems on Putnam 2025, 4 out of 6 on IMO 2025, and 3 out of 6 on USAMO 2026[1][2].
benchmarkresearch-papertool-release
Background sources we checked (1)
- arxiv.org ↗ 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 perf…