L$^2$EAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present L$^2$EAP (LLM-in-Lean Environment Agentic Prover), an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. L$^2$EAP 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, L$^2$EAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models; on Lean-IMO-Bench, L$^2$EAP raises the one-shot formal solve rate of general-purpose LLMs from below 10\% to 70\%. It also compares favorably to the best baseline performance of 48\% attained by a specialized system with dedicated ATP components that achieved gold-medal-level performance at the 2025 IMO.