# APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning arXiv: https://arxiv.org/abs/2505.05758 ยท HTML: https://mlsanity.com/paper/2505.05758/ ## Key facts - Cited by 35 papers in the map (data through 14 Oct 2026). - Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. - Builds on 3 of its 45 references that are in the map. - First posted on arXiv 9 May 2025. ## Placed in - LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/) ## Builds on (most cited first, 3 of 3) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023) - [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024) - [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025) ## Built on by (most cited first, 30 of 35) - [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025) - [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025) - [Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries](https://mlsanity.com/paper/2606.10402/) (2026) - [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026) - [Process-Verified Reinforcement Learning for Theorem Proving via Lean](https://mlsanity.com/paper/2606.20068/) (2026) - [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025) - [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026) - [Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning](https://mlsanity.com/paper/2601.00791/) (2026) - [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026) - [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026) - [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026) - [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026) - [ProofCompass: Enhancing Specialized Provers with LLM Guidance](https://mlsanity.com/paper/2507.14335/) (2025) - [Automated QoR improvement in OpenROAD with coding agents](https://mlsanity.com/paper/2601.06268/) (2026) - [Clarifying Before Reasoning: A Coq Prover with Structural Context](https://mlsanity.com/paper/2507.02541/) (2025) - [Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving](https://mlsanity.com/paper/2604.01483/) (2026) - [AI-Assisted Discovery of Convex Relaxations via Dual Agents](https://mlsanity.com/paper/2606.31182/) (2026) - [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026) - [TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow](https://mlsanity.com/paper/2601.17332/) (2026) - [MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving](https://mlsanity.com/paper/2603.24465/) (2026) - [Toward Evaluation Frameworks for Multi-Agent Scientific AI Systems](https://mlsanity.com/paper/2603.26718/) (2026) - [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026) - [Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search](https://mlsanity.com/paper/2605.20244/) (2026) - [TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics](https://mlsanity.com/paper/2606.09450/) (2026) - [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026) - [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026) - [Provably Complete Generalized Planning with LLMs](https://mlsanity.com/paper/2609.27105/) (2026) - [Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)](https://mlsanity.com/paper/2602.18918/) (2026) - [Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs](https://mlsanity.com/paper/2605.04472/) (2026) - [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026) ## Abstract (arXiv) Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal languages like Lean. A formal verification system can check whether a formal proof is correct or not almost instantaneously, but generating a completely correct formal proof with large language models (LLMs) remains a formidable task. The usual approach in the literature is to prompt the LLM many times (up to several thousands) until one of the generated proofs passes the verification system. In this work, we present APOLLO (Automated PrOof repair viaLLM and Lean cOllaboration), a modular, model-agnostic agentic framework that combines the strengths of the Lean compiler with an LLM's reasoning abilities to achieve better proof-generation results at a low token and sampling budgets. Apollo directs a fully automated process in which the LLM generates proofs for theorems, a set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal with a low top-K budget. The repaired sub-proofs are recombined and reverified, iterating up to a user-controlled maximum number of attempts. On the miniF2F benchmark, we establish a new state-of-the-art accuracy of 84.9% among sub 8B-parameter models (as of August 2025) while keeping the sampling budget below one hundred. Moreover, Apollo raises the state-of-the-art accuracy for Goedel-Prover-SFT to 65.6% while cutting sample complexity from 25,600 to a few hundred. General-purpose models (o3-mini, o4-mini) jump from 3-7% to over 40% accuracy. Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness, suggesting a general paradigm for scalable automated theorem proving.