APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Authors: Azim Ospanov
Farzan Farnia
Roozbeh Yousefzadeh
Venue: NeurIPS 2025 poster ()
Keywords: formal reasoning
automated theorem proving
lean prover
ai for math
Primary area: machine_learning_for_sciences

Abstract: 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 (**A**utomated **P**r**O**of repair via**L**LM and **L**ean c**O**llaboration), 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. The codebase is available at https://github.com/aziksh-ospanov/APOLLO

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Azim Ospanov *f aospanov9@cse. cuhk edu hk
Farzan Farnia farnia@cse. cuhk. cuhk edu hk
Roozbeh Yousefzadeh roozbeh. yr@ghail. com
Abstract
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 formidable task. The usual approach the literature is to prompt the LLM many times (up to several thousands) until one of the generated proofs passes the verifi- cation system. In this work, we present APOLLO (Automated PrOof repair via LLM and Lean cOllaboration), modular, model-agnoste agentic framework that combines the strengths of the Lean compiler with an LLM's reasoning abilities to achieve better proof-generation results at low token and sampling budgets. Apollo directs a fully automated process in which the LLM generates proofs for theorems, 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 LLM on each remaining goal with low top-K budget. The repaired sub-proofs are recombined and reverified, iterating to user-controlled maximum number of attempts. On the miniF2F benchmark, we establish new state-of-the-art accuracy of 84.9% among sub 8B 3B-parameter models (as of August 2025) while keeping the sampling budget below one hundred. Moreover, Apollo raises the state-of-the-art accuracy for
to 65.6% while cutting sample complexity from 25,600 to few hundred. General-pun pprrpos models (o3-mini, o4-mini) jump from 3-7% to over 40% accuracy. Our results demonstrate that targeted, compiler-guiee -uidee repair LLM outputs yields dramatic gains both efficiency and correctness, sug- gesting general paradigm for scalable automated theorem proving. The codebase is available lhttp::/ tht.. com/azikeeeeeeeoooooo ksh ospanov/APOLLO
1 Introduction
Formal reasoning has emerged as one of the most challenging fields of AI with recent achievements such AlphaProof and AlphaGeometry doing well the International Math Olympiad competing with humans 11 3) Formal reasoning relies both on Al models and formal verification system that can automatically verify whether a mathematical proof correct or not. recent years, formal verification systems such as Lean 4 have facilitated new form of doing mathematical research by enabling mathematicians to interact with the formal verification system and also with each other via the system, enabling larger numbers of mathematicians to collaborate with each other a single project. As such, these formal verification systems are also called proof assistants as one can use them interactively to write a formal proof and instantaneously observe the current state of the proof and any possible errors or shortcomings in the proof generated by the compiler. Immediate access
Huawei Hong Kong Research Center
Department of Computer Science & Engineering, The Chinese University of Hong Kong
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

Common Approach: Whole-Proof Generation Pipeline
repeat up to K times
poont stlenpe
Our Proposed Apollo Pipeline
repeal up times
LLM
Apolio Frred Repair Agent
Lean Server
prosf Mtle
sub-gniclanial prace
campiiation wylts ento
Suliiee
Indyyrd Extata
Figure I: The summary of whole-proof generation pipeline vs. proposed Apollo agentic pipeline. LLM refers chosen formal theorem generator model.
to the output of Lean compiler help mathematician to fix possible errors in the proof. At the same time, when proof passes the compiler with no error, other collaborators do not need to verify the correctness of the proof. This type of collaboration is transforming the field of mathematics enabling large groups of collaborators to engage in large projects of mathematical research such as the Prime Number Theorem And More project [5). Moreover, it has given rise the digitization of mathematics [
In the AI front, large language models (LLMs) are improving at mathematical reasoning in natural language, and at the same time, they have shown remarkable ability to learn the language those formal verification systems and write mathematical proofs in formal language. This has led to the field Automated Theorem Proving (ATP) where the standard approach is to prompt the LLM to generate number of candidate proofs for given theorem which will then be verified automatically using the formal verification system. Better models, better training sets, and better training methods has led significant advances in this field
Despite these advances, the LLMs do not really get the chance to interact with the verification system the way human does. LLMs generate many possible proofs, sometimes many as tens of thousands, and the verification system only marks the proofs with binary value correct or incorrect. This common approach is illustrated in Figure When the formal verification system analyzes proof, its compiler may generate long list of issues including syntax errors, incorrect tactics, open goals, etc. In the current approach of the community, all of those information/fecdback from the compiler remains unused, as the LLM's s proof generation is not directly engaged with the compiler errors of the formal verification system.
In this work, we address this issue by introducing Apollo, a fully automated system which uses a modular, model-agnostic pipeline that combines the strengths of the Lean compiler with the reasoning abilities of LLMs. Apollo directs fully automated process in which the LLM generates proofs for theorems, 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 low top-K budget. The high-level overview of Apollo appears the bottom of Figure

---

Our contributions are as follows:
We introduce novel fully automated system that directs a collaboration between LLMs, Lean compiler, and automated solvers for automated theorem proving.
We evaluate Apollo miniF2F-test set using best LLMs for theorem proving and demonstrate that Apollo improves the baseline accuracies by significant margins while keeping the sampling costs much lower.
We establish a new SOTA on miniF2F-test benchmark for medium-sized language models, (with parameter size 8B or less)
2 Related Works
Formal theorem proving systems. At their core, formal theorem-proving (FTP) systems employ interactive theorem provers (TTPs) to verify mathematical results. In particular, Lean4 [4] is both a functional programming language and an ITP. Each theorem, lemma, conjecture, or definition must be checked by Lean's 's trusted kernel, so the compiler's verdict is binary: either the statement type-checks (True) or it fails (False). This rigorous verification dramatically increases the reliability of formal mathematics; however, it also increases the complexity of proof development: authors must both comprehend the mathematical concepts and precisely encode them in the formal language. The usefulness of Lean is also shown to go beyond theorem proving, Jiang al. 12 showed that Lean can be adapted to natural language logical reasoning.
Patching broken programs. Many prior works have explored using feedback to repair broken proofs. In software engineering, "repair" typically refers to program repair, i.e. fixing code that no longer runs 13. A common source of errors is version mismatch that introduces bugs and prevents execution. For example, SED 14] uses a neural program- -egrraamggeerttionn pipeline that iteratively repairs initial generation attempts. Other notable approaches train specialized models fix broken code based on compiler feedback (e.g. BIFI [15), TFix (16) or leverage unsupervised learning over large bug corpora (e.g. BugLab 17)).
LLM collaboration with external experts. The use of expert feedback, whether from human users or from a proof assistant's 's compiler, has proven effective for repairing broken proofs. Ringer [18] showcased automatic proof repair within the Coq proof assistant [99] enabling the correction of
proofs in response to changes in underlying definitions. Jiang et al. 20 showed that leveraging automatic solvers with generative models yield better performance on formal math benchmarks. More recently, First al. [2 showed that incorporating compiler feedback into LLM proof generation significantly improves the model's 's ability to correct errors and produce valid proofs. Another line of work 22 explored an idea of mathematician and LLM collaboration, where human experts are aided by LLMS at proof writing stage.
Proof search methods. Numerous recent systems machine learning to guide the search for formal proofs. One of the methods involves using large language models with structured search strategies, e.g. Best-Firrt Search (BFS) 23
24 2 Monte Carlo Tree Search (MCTS) [26] 27 2]. While tree-search methods reliably steer model toward valid proofs, they result in high inference costs and often explore many suboptimal paths before success. Another line of work leverages retrieval based systems to provide context for proof generators with potentially useful lemmas. One such example is ReProver (28) that augments Lean proof generation by retrieving relevant lemmas from proof corpus and feeding them to an LLM, enabling the model to reuse existing proofs.
Whole proof generation. The use of standalone LLMs for theorem proving has emerged as major research direction in automated theorem proving. One of the carliest works presented GPT-f [29], a transformer-basee model for theorem proving that established the LLMs ability in formal reasoning. As training frameworks and methods advance, the community has produced numerous models that generate complete proofs without external search tree-search algorithms. Recent work shows that
both supervised models [30] 31 and those trained via reinforcement learning [30 32 33 34 achieve competitive performance formal-man benchmarks. However, whole-proof generation remains vulnerable to hallucinations that can cause compilation failures even for proofs with correct reasoning chains.
Informal Chain-of- Thon-ght in Formal Mathematics. Several recent works demonstrate that interleaving informal "chain-of-though (CoT) reasoning with formal proof steps substantially

---

Apollo Algorithm
Syntax Refiner
Sorrifier
Auto Solver
Edtrect vetgponts
Feed
NOB
Proof Assembler
sumber atteppls> 1
comple
YESB
Socalid Proo!
Correc
LC
Jenay
a0e Linentth
Chanzen mattd wwwberttorryyy.oooooooooo 411 Sensrrect (a
[bc]
hane 17 120
Da sat. god a 20X lec
hane it
hove
[mm]
by
bars
[b9]
b7.00mtrx
byy cenkee
peak,
Monetch
Jame
[h)
bax
Learrthh
spple and 1o.rigt
Jare bas 129
buridin ERL and
by 2y_0occze
Latervel_caae cseps
buzidtn IEL. and FOR buizete) Isternal COEEE TIN Inseeve: SAR8E
42% try ( conccediction
<th try 3 cecsentiction)
Figure Overview of the Apollo framework.
improves whole-proof generation. For example, developers insert natural- mathematical commentary between tactics, yielding large accuracy gains [31 30 35). Wang, et al. [44] further show that special "thinking" tokens let the model plan its strategy and self velf-verify intermediate results. The "Draft, Sketch, and Prove" (DSP) [36] and LEGO- Prover 37 pipelines rely on an informal proof sketch before attempting generate the formal proof. Collectively, these studies indicate that providing informal mathematical context, whether as comments, sketches, or dedicated tokens, guides LLMs toward correct proofs and significantly boosts proof synthesis accuracy.
3 Our Approach
In this section we describe Apollo, our framework for transforming an LLM's raw proof sketch into a fully verified Lean4 proof. Figure[jillustrate the Apollo pipeline process with an attached Lean code before and after repair. We observe that often LLM is capable of producing a valid proof sketch; however, it often struggles with closing fine-grained goals. For example, statements h4, h5, h7, h8 are correct but the generated proofs for each sub-lemma throw compilation errors. Apollo identifies and fixes such proof steps and guides the LLM towards a correct solution.
Our compiler of choice is the Lean REPL (38], a "Read Evall Wral-Print--ee Loop"" for Lean4. provides a complete list of compilation errors and warnings, each with detailed description and the location (for example, the line number) where it occurred. Errors can include syntax mistakes, nonexistent tactics, unused tactics, and more. We aggregate this information to drive our agent's dynamic code repair and sub-problem extraction. The pseudo-code for our framework can be found in Algorithm in the Appendix.

---

3.1 Syntax Refiner
The Syntax Refiner catches and corrects superficial compilation errors: missing commas, wrong keywords (e.g. Lean3's from vs. Lean4's by), misplaced brackets, etc. These syntax errors arise when a general-purpose LLM (such as o3-mini [39 or 04-mini (40) has not been specialized on Lean4 syntax. By normalizing these common mistakes, this module ensures that subsequent stages operate on syntactically valid code. is important to note that this module primarily applicable to general purpose models not explicitly trained for theorem proving in Lean. In contrast, Syntax Refiner usually does not get invoked for proofs generated by LLMs trained for formal theorem proving.
3.2 Sorritier
The Sorrifier patches any remaining compilation failures by inserting Lean's sorry placeholder. We first parse the failed proof into a tree of nested proof-blocks (sub-lemmas as children). Then we compile the proof with Lean REPL. (38, detect the offending line or block, and apply one of three repairs:
1. Line removal, if single tactic declaration is invalid but its surrounding block may still succeed.
2. Block removal, if the entire sub-proof is malformed.
3. Insert sorry, if the block compiles but leaves unsolved goals open.
We repeat this procedure until the file compiles without errors. At that point, every remaining sorry marks a sub-lemma to be proved in later stages of Apollo. This part of the pipeline guarantees that the proof successfully compiles in Lean with warnings of presence sorry statements.
Each sorry block corresponds to a sub-problem that the LLM failed to prove. Such blocks may not type-check for various reasons, most commonly LLM hallucination. The feedback obtained via REPL lets us to automatically catch these hallucinations, insert a sorry placeholder, and remove invalid proof lines.
3.3
Auto Solver
The Auto Solver targets each sorry block in turn. It first invokes the Lean4's hint to close the goal. If goals persist, it applies built-in solvers aolinarith, ring, simp, etc.) wrapped in try to test combinations automatically. Blocks whose goals remain open stay marked with sorry. After applying Auto Solver, a proof may be complete with no sorry's in which case Apollo has already succeeded in fixing the proof. Otherwise, the process can repeat recursively.
3.4 Recursive reasoning and repair
In the case where proof still has some remaining sorry statements after applying the Auto Solver, Apollo can consider each as new lemma, i.c., extract its local context (hypotheses, definitions, and any lemmas proved so far), and recursively try to prove the lemmas by prompting the LLM and repeating the whole process of verification, syntax refining, sorrifying, and applying the Auto Solver.
At each these recursive iterations, a lemma may be completely proved, or it may end up with an incomplete proof with one or few sorry blocks. This allows the Apollo to make progress in proving the original theorem by breaking down the incomplete steps further and further until the LLM or Auto Solver can close the goals. This process can continue up to a user-specified recursion depth r.
3.5 Proof Assembler
Finally, the Proof Assembler splices all repaired blocks back into a single file and verifies that sorry admit (alias for "sorry") commands remain. If the proof still fails, the entire pipeline repeats (up to a user-specified recursion depth r), allowing further rounds of refinement and sub-proof generation.
Apollo's staged approach: syntax cleaning, "sorrifying." automated solving, and targeted L.-M-driven repair, yields improvements in both proof-sample efficiency and final proof correctness.
5

---

Experiments
In this section, we present empirical results for Apollo on the miniF2F dataset [8, which comprises of 488 formalized problems drawn from AIME, IMO, and AMC competitions. The benchmark is evenly split into validation and test sets (244 problems each); here we report results on the miniF2F-ttst parti- tion. To demonstrate Apollo's effectiveness, we evaluate it on range of state-of-the-art whole-proof generation models. All experiments use Lean 14.1 and run on eight NVIDIA A5000 GPUs with 128 CPU cores. We used @32 sampling during sub-proof generation unless stated otherwise. Baseline numbers are sourced from each model', 's original publication works.
4.1 The effect of applying Apollo on top of the hase models
Figure shows the impact of Apollo on two state-of-the-art whole-proof generation models: Goedel Prover-SFT [3 and
34 Applying Apollo increases Goedel-Prover-SFTT top accuracy from 64.7% to 65.6% while reducing its sampling budget by two orders of magnitude (from 25,600 generated samples to only few hundred on average). Similarly, accuracy
Prover-Preview-Dee
achieves new best Kimina-Prover Previ-r--eviiiiiee of 75.0% with roughly one-third of the previous sample budget. We report the exact numbers in Table 1
Prover-Preview-DDe
Performance of Goedel-Prover-SFT
Performance of Priiia-Prover-Preview---D-
Provor Disill
Kimins Prevlew Distil Agollo
64-
Accuracy (%0)
62-
60-
Goodel Gowdee-rovee-SFT
18
25.d
200
600
1000
budget (I)
Pass budget (K) log scale
(a) Model accuracy against sampling budget
Performance of
Performance of Kimina Previee-rei
Accuracy (%)
72
62
60-
Goedel Prover SFT
Kimins Prover Preview Distil-7 7B
Goodal Prover SFT Acolo
Kimina Prover-Previoe Di:il-78 Proviow-D:dll-78 Apolo
1617
140.00 mk
4as
134
4.94
12774
140.00
socar
A.M
Taken budget (N) log scale
Token budget (N) log scale
(b) Model accuracy against generated token budget
Figure 3: Performance of base models against the Apollo aided models on miniF2F-test dataset at different sample budgets and token length.
Note that Apollo's sampling budget is not fixed: it depends on the recursion depth and the LLM's ability to generate sub-lemmas. For each sub-lemma that Auto Solver fails to close, we invoke the LLM with fixed top-32 sampling budget. Because each generated sub-lemma may spawn further sub-lemmas, the total sampling overhead grows recursively, making any single @ K budget difficult to report. Sub-lemmas also tend to require far fewer tactics (and thus far fewer tokens) than the main theorem. theorem might need 100 lines of proof while sub-lemma might need only line. Hence, sampling cost does not scale one-to-one. Therefore, to compare with other whole-proof generation

---

Table I: Table results comparing sampling cost, accuracy, and token usage before and after ap- plying Apollo. "Cost" denotes the sampling budget K for whole-proof generation and the recur- sion depth for Apollo. Column N reports the average number of tokens generated per problem in "Chain-of-Thirn Thoughtt mode. Bold cells highlight the best accuracy. Results are shown on the miniF2F-test dataset for two models:
Leover-Preview-ioe
and Goedel-SFT.
Goedel-
Kimina-Prover- Prover-Previeew
Base Model
+ Apollo
Base Model
Apoolo
N
Acc. (%)
T
N
Acc. (%)
K N
Acc. (%)
r
Acc. (%)
32
16.1K
57.6%
0
16.1K
57.6%
32
140K
63.1 1%
140K
63.1%
64
31.8K
59.2%
2 38.3K
60.7%
406K
68.9%
3200
1.6M
62.7%
4 74.6K
63.5%
816K
74.2%
25600
12.7M
64.7%
6. 179.0K
65.6%
1024 4.5M 70.8%
1.3M
75.0%
approaches, we report the average number of proof samples and token budgets. We present more in-depth analysis of inference budgets in Section B of the Appendix.
4.2 Comparison with SoTA LLMS
Table compares whole-proof generation and rearch methods miniF2F-test. For each approach, we report its sampling budget, defined as the top-K parameter for LLM generators or equivalent search-depth parameters for tree-search provers. Since Apollo's budget varies with recursion depth r, we instead report the mean number of proof sampled during procedure. Moreover, we report an average number of generated tokens as another metric for computational cost of proof generation. For some models due to inability to collect generated tokens, we leave them blank and report sampling budget only.
When Apollo is applied on top of any generator, it establishes a new best accuracy for that model. accuracy jumps 65.6%, surpassing the previous best result
For instance, fooedel-Prover-S- (which required 25,600 sample budget). In contrast, Apollo requires only 362 samples on average. Likewise, Kimina- Preinna--rrre--Peeeee Preview-Distill.
sees a 4.2% accuracy gain while reducing its sample budget below the original 1,024. To further validate Apollo's generalizability. we tested the repair framework on Goedel-V2-80 41), the current -fate-of-the-art theorem prover. We observe that, at similar sample and token budgets, Apollo achieves a 0.9% accuracy gain, whereas the base LLM requires twice the budget to reach the same accuracy. Overall, Apollo not only boosts accuracy but does so with a smaller sampling budget, setting new ttate-of-the-art result among sub-8B-pan -paammtter LLMs with sampling budget of 32.
We also evaluate general-purposs. LLMS (OpenAl 03-mini and o4-mini). Without Apollo, these models rarely produce valid Lean4 proofs, since they default to Lean3 syntax or introduce trivial compilation errors. Yet they have a remarkable grasp of mathematical concepts, which is evident by the proof structures they often produce. By applying Apollo's syntax corrections and solver-guided refinements, their accuracies increase from single digits (3-7%) to over 40%. These results demon- strate that in many scenarios discarding and regenerating the whole proof might be overly wasteful, and with a little help from a Lean compiler, we can achieve better accuracies while sampling less proof's from LLMs.
To further assess Apollo, we conducted experiments on PutnamBench 771. using Simina-Provees Preview-Distill-777 the base model. Under whole-proof generation pipeline, LLM produced 10 valid proofs. With Apollo, the LLM produced one additional valid proof while consuming nearly half many tokens. Results are presented in Table 3
Overall, our results on a variety of LLMs and benchmarks demonstrate that Apollo consistently consumes fewer tokens while achieving higher accuracy, highlighting its effectiveness.
4.3 Distribution of Proof Lengths
We assess how Apollo affects proof complexity by examining proof-length distributions before and after repair. Here, proof length is defined as the total number of tacties in a proof, which serves as a proxy for proof complexity.
7

---

Table 2: Comparison of Apollo accuracy against state-of-the-art models on the miniF2F-test dataset. Token budget computed over all generated tokens by L.M.
Method
Model size
Sample budget
Token budget
miniF2F-test
Tree Search Methods
Hypertree Proof Search 26
0.6B
64 x 5000
41.0%
MILLM..5-SP-BFS-E
24
7B
256 x 32 x 600
65.9%
HPv16+BBS+DD 421
7B
600 x 8 400
68.4%
BFS-Prover 25
7B
2048 x 2 600
70.8%
Whole-proof Generation Methods
DeepSeek-RI-
7B
32
42.6%
Distill-Qwen-7B
43
Leanabell-GD
32
7B
128
61.1%
STP 33
25600
67.6%
1
3.3%
03-mini
39
32
24.6%
04-mini 40
7.0%
32
16.1K
57.6%
Goedel-SFT 3
7B
3200
1.6M
62.7%
25600
12.7M
64.7%
1
4,4K
52.5%
Kimina-Proven
7B
32
140K
63.1%
Preview-Distill
1024
4.5M
70.8%
32
174K
83.3%
Goedel- V2 41
8B
64
349K
84.0%
128
699K
84.9%
Whole Generation Methods + Apollo
03-mini Apollo
8
40.2% (+36.9%)
04-mini + Apollo
15
46.7% (+39.7%)
Goedel-SFT + Apollo
7B
362
179K
65.6% (+0.9%)
PiniinaPreevewwaae Apollo
307
1.3M
75.0% (+4.2%)
Goedel-V2 Apollo
8B
63
344K
84.9 % (+0.9%)
Table 3: Comparison of Apollo accuracy the PutnamBench dataset. Token budget is computed over all generated tokens by LLM.
Method
Model size
Sample budget
Token budget
PutnamBench
Kimina- Menina-Preview
7B
32
180K 1.1M
7/658
Kimina-Par Previee
7B
192
10/658
Priina-Preview+Apollo
7B
108
579K
11/658
Figure presents violin plots for three base models: Kimina Prover-Preview-Diie Goedel-Prover-SFT. and o4-mini. Each subplot shows two non-overlapping sets: proofs gener- ated directly by the base model ("before") and proof' produced after applying Apollo ("afteer"). We only consider valid proofs verified by REPL in this setup.
The proofs that Apollo succeeds in fixing in collaboration with the LLM have considerably longer proof lengths. The mean length of proofs fixed by Apollo is longer than those written by the LLM itself at least by a factor two in each model selection scenario. This increase indicates that proofs which the base model alone could not prove require longer, more structured reasoning chains. By decomposing challenging goals into smaller sub-lemmas, Apollo enables the generation of these extended proofs, therefore improving overall success rate.

---

These results demonstrate that Apollo not only raises aceuracy but also systematically guides models construct deeper, more nigoouus proof structures capable of solving harder theorems.
Moee 35.1
Maxe 664
Marro
Mas 330
Moar
Maue 160
25
(a) Kimina-Preview-Distii
(b) Goedel-SFT
(c) OpenAl o4-mini
Figure 4: Distribution of proof lengths for selected models before (left) and after (right) applying Apollo. In the "before" plots, proof lengths cover only proofs the base model proved without the help of Apollo; in the "after" plots, proof lengths cover only proofs proved with Apollo's assistance.
4.4 Impact of recursion depth r on proof accuracy
We evaluate how the recursion-depth parameter r affects accuracy on minil2 A recursion depth of r 0 corresponds the base model's standalone performance; higher values permit additional rounds of Apollo. plptts accuracy versus r for three models: 04-mini (r = 0...4). 0).
Prover-reevieeww
(r 0...6), 6), and Goedel-PPover-SFFT
The o4-mini model exhibits its largest accuracy gain between r = 0 and r = 1, since its raw proof structure is often correct but contains many syntax errors and proof-step errors. Syntax Refiner fixes most of them and together with Auto Solver leads to a spike in accuracy. Beyond r = 1, accuracy plateaus, since 04-mini not explicitly designed for proving formal theorems. We note that even though accuracy gains slow down drastically for 04-mini, its accuracy still increases at a slow rate, which means that pushing parameter r further has potential increase the efficiency of o4-mini further. In contrast, both Kimina-Proved Prover-rrevieew----- improve steadily throughout different levels of recursion depth. The results suggest that decomposing the challenging problems into smaller parts allows the model to close simpler goals, slowly building towards a complete proof.
and Goedel-Prover-STT continue to
Although the total number of proof samples grows with r, even r = 5 requires only 300-400 LLM requests average, order of magnitude below typical budgets in the literature. Moreover, one could further increase Y' to explore budgets in the thousands if desired.
4.5 Ablation Studies on different components of Apollo
To evaluate the contribution of each Apollo component, we conducted an ablation study on two base models: 04-mini (a general-purpose model) and Praiia--rover-Prevvewwe
(a theorem-prover model). Results are reported Table 4 We decomposed Apollo into three key modules: Syntax Refiner, Auto Solver, and LLM Re-invoker. The LLM invoker is the module which re-invokes the LLM to prove the sorrified sub-goals. The Sorrifier and Proof Assembler modules are excluded from this analysis, they essential for decomposing problems into sub-goals and assembling proofs, and thus cannot be ablated.
04-mini
Goedel-Proverr SFT
Mimnina-Prover-Peeee Distill----
Tacursion Degth
Rauuratn Degth
Bacurskrr Duphh
Figure 5: Performance of Apollo miniF2F dataset at various recursion depth parameters on three different models: 04-mini, Kimina-Prowt Prover- Srevvee--isttll.. and Goedel-Prover-S Prover-SFT.

---

From the results, we observe that Syntax Refiner alone provides only marginal benefit, and its effect is limited to the peneral-purpose model 04-mini; it yields no improvement on the dedicated prover. Auto Solver, when used in isolation, also produces little accuracy gain, indicating that built-in solvers in most cases do not have the capability to prove the failed sub-goals after the first round of proof generation by LLMs. However, further reasoning and proof decomposition on those sub-goals by the LLM can significantly increase the accuracy gain. The most significant accuracy gains, however, arise when Auto Solver and LLM Re-invoker are combined, which corresponds to the full Apollo framework. This demonstrates that Apollo's repair mechanism crucial for achieving robust performance across both model types. We extend the ablation to individual module triggers during inference Section E of the Appendix.
Table 4: Ablation study of different parts of Apollo on o4-mini (general purpose model) and Kimina- Moover-rrvveew-Distlleee (theorem prover model).
Apollo Modules
Model Accuracy
Syntax Refiner
AutoSolver
LLM Re- Invoker
04-mini
Kimina-7B
x
X
7.0%
63.1%
X
7.4%
63.1%
X
7.0%
63.5%
X
X
8.2%
69.3%
X
20.5%
63.5%
X
V
18.9%
69.3%
10.2%
75.0%
46.7%
75.0%
Limitations
Integration with tree-search methods. Our evaluation focuses exclusively applying Apollo to whole-proof generation by LLMs and does not explore its interaction with traditional tree-search provers (e.g. BFS, MCTS). Investigating how lemma decomposition and targeted repair could accelerate or prune search paths in those systems a promising direction for future work.
Dependence on base model's proof sketch quality. Apollo's ability to produce a correct formal proof largely depends on the base model and whether its initial proof has a coherent proof sketch. As 44 observe, models often tend to "cut corners," producing proofs that are much shorter than the rigorous, multi-step arguments required to generate a valid proof. When base model fails to write correct proof strategy (e.g. omitting critical lemmas suggesting irrelevant tactics, taking wrong approach), the Apollo is less likely to repair such proof. Enhancing the robustness of Apollo to very poor initial sketches remains open challenge.
Conclusion
In this work, we present Apollo, novel, modular fully automated agentic system that combines syntax cleaning, automatic solvers, and LLM-ddrven sub-proof generation to transform an LLM's initial proof sketch into fully verified Lean4 proof. This framework harnesses the full power of the Lean compiler and integrated solvers, merging them with L.MM systems. Applied across five whole-proot generation models, ranging from general-purpose LLMs (o3-mini, o4-mini) specialized provers (Kimina-PPi Proiee-rrvv--eeee Prover-Preview-DDe Preview-Distill-77 new best accuracies on the miniF2F benchmark while reducing token and sampling budgets by one to two orders of magnitude. Our empirical analysis shows that Apollo not only raises overall proof success rates but also guides models to generate longer. more structured proofs, as evidenced by drastic increase in average successful proof length. We further demonstrate how the recursion- depth parameter r trades off sample complexity against accuracy, achieving robust gains with only a few hundred samples. We believe that Apollo's collaboration between L.MSs, automatic solvers, and the Lean compiler defines paradigm of agentic systems that produce high-quality, verifiable proofs for increasingly challenging theorems.
Prover-SFT, Goedel-V2), Apollo consistently establishes
10

---

Acknowledgments
The work of Farzan Farnia is partially supported by a grant from the Research Grants Council of the Hong Kong Special Administrative Region, China, Project 14209920, and is partially supported by CUHK Direct Research Grants with CUHK Project No. 4055164 and 4937054. Also, the authors would like to thank the anonymous reviewers for their constructive feedback.
References
[1] Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI. In Proceedings of the International Conference on Machine Learning. 2025.
[2] Google DeepMind. AI achieves silver-medal standard solving international math- ematical olympiad problems.
https://dsepming google/discover/////eeeooooo ai-solves- imo -wr-iiioooooomss---e---- -t---ttt-slllee www.-ssseeeeeeaaaleeeeeee
2024. Accessed: 2025-05-
08.
[3] Trieu Trinh, Yuhuai Wu, Quoc Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations, Nature, 2024.
[4] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. Automated Deduction CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, page 625-635, Berlin, Heidelberg, 2021. Springer-
[5] Alex Kontorovich and Terence Tao. Prime number theorem and more. htttps://githun com/ 2024. Version 0.1.0, .0, released 2024-01-09.
[6] Kevin Buzzard. Mathematical reasoning and the computer. Bulletin of the American Mathemat- ical Society, 2024.
[7] George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition, 2024.
[8] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: cross-system benchmark for formal Olympiad-level mathematics, 2022.
[9] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leve mathematics, 2023.
[10] Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu. Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleurcau, Guillaume Lample. and Stanislas Polu. Numina- math. petpps//ggtiie report/numina, www.iauminnaaaaaammmmmmaa dataset... pdf 2024. GitHub repository.
com/ commprojectt..... hetojjjettnumina//// numina/ awmaaammmaaaeeeeee proggrsss-prize/llotee
[11] Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Jcontexts. In The Thirteenth International Conference on Learning Representations, 2025.
Neural theorem proving with (long-
[12] Dongwei Jiang, Marcio Fonseca, and Shay B Cohen. Leanreasoner: Boosting complex logical reasoning with lean. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pages 7490-7503, 2024.
[13] Quanjun Zhang, Chunrong Fang, Yuxiang Ma, Weisong Sun, and Zhenyu Chen. A survey of learning-baad automated program repair. ACM Trans. Softw Eng. Methodol, 33(2), December 2023.
11

---

[14] Kavi Gupta, Peter Ebert Christensen, Xinyun Chen, and Dawn Song. Synthesize, execute and debug: Learning repair for neural program synthesis. Advances Neural Information Processing Systems, volume 33, pages 17685-17695. Curran Associates, Inc., 2020.
[15] Michihiro Yasunaga and Percy Liang. Break-it-fix-it. Unsupervised learning for program repair. In Proceedings of the 38th International Conference on Machine Learning, volume 139, pages 1 11941-11952. PMLR, 18-24 Jul 2021.
[16] Berkay Berabi, Jingxuan He, Veselin Raychev, and Martin Vechev. Tfi: Learning fix coding errors with a text-to-text transformer. In Proceedings of the 38th International Conference on Machine Learning, volume 139, pages 780-791. PMLR, 18-24 Jul 2021.
[17] Miltiadis Allamanis, Henry Jackson-Flux. and Mare Brockschmidt. Self-supervised bug de- tection and repair. In Advances in Neural Information Processing Systems, volume 34, pages 27865-27876. Curran Associates, Inc., 2021.
[18] Talia Ringer. Proof Repair. PhD thesis, University of Washington, 2021. Ph.D. dissertation.
[19] Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.
[20] Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski. Tomasz Odrzyg62dZ, Piotr Miloš, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Advances in Neural Information Processing Systems, 2022.
[21] Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models, 2023.
[22] Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean. In The 3rd Workshop on Mathematical Reasoning and Al at NeurlPS 23, 2023.
[23] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
[24] Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen, thtemlm2.5-stepprooeer Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024.
[25] Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. BFS-Prover: Scalable best-first tree search for Ilm-based automatic theorem proving, 2025.
[26] Guillaume Lample. Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. In Proceedings the 36th International Conference Neural Information Processing Systems, pages 26337-26349, 2022.
[27] Haiming Wang et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61 Annual Meeting of the Association for Computational Linguistics (Volume 1: Longg Pupers), pages 12632-12646, 2023.
[28] Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval- Augmented Language Models, October 2023. Sidi::2306116226
[29] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
[30] Huajian Xin, Z. Z. Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang. Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Prepseek-prover-ye for reinforcement learning and monte-carlo tree search, 2024.
Harnessing proof assistant feedback
12

---

[31] Yong Lin, Shange Tang. Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. -redel-prover: frontier model for open-source automated theorem proving, 2025.
[32] Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prooer: Posttraining scaling in formal reasoning, 2025.
[33] Kefan Dong and Tengyu Ma. STP: Self-play LLM theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.002:2 2025.
[34]
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying. Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidr, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang. Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, and Jia Li. Kimina-Prover Preview: Towards large formal reasoning models with reinforcement learning. 2025.
[35] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang. Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations, 2024.
[36] Albert Q. Jiang et al. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs, 2023.
[37] Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. LEGO-pret prover: Neural theorem proving with growing libraries. The Twelfth International Conference on Learning Representationss 2024.
[38] Lean FRO. A uand-eval-rrint-lon for Lean 4.
https://githun com/
leanprover - community/rep 2023.
[39] OpenAL. Openai o3-mini. nuttps://opan com/ index/ comaadeee///oaoaaaaiiiiiii 03-mini/ January 2025.
[40]
OpenAl. Introducing openai o3 and 04-mini.
April 2025.
[41] Yong Lin, Shange Tang. Bohan Lyu, Ziran Yang. Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Grover--: The strongest open-source theorem prover to date, 2025.
[42] Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang. and Haitao Mi. Hun- yuanProver: A scalable data synthesis framework and guided tree search for automated theorem proving, 2025.
[43] DeepSeek-AI. DeepSeek-R1: Incentivizing reasoning capability in lims via reinforcement
learning, 2025.
[44] Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems. Transactions on Machine Learning Research, 2025.
[45] Huajian Xin, 7. 7. Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao, Haocheng Wang. Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, 7. Wu, Fuli Luo, and Chong Ruan. PeepSeek-Prover-VI Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search, August 2024, arXiv:2408.08155
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
The paper presents a novel framework for proof generation that is compatible with any whole-proof generation LLM. Main claims are supported by experimental results different base LLMs.
Justification:
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
In the paper we discuss the limitations of ProofRepair in variety of settings.
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model sell-speciiiaatinn asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
14

---

Answer: [NA]
Justification: Presented framework does not rely on theoretical results and instead presents practical sample complexities for whole-proof generation.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proof' in the paper should be numbered and cross referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Question:
Answer: [Yes]
Justification: The paper presents all hyperparameters and sampling budgets needed to replicate the results.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reprodueibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
15

---

Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
The submission comes with demo code to run and reproduce the main experimental claims.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to rum to reproduce the results. See the NeurIPS code and data submission guidelines (https
for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing much information possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Question:
Answer: [Yes]
Justification:
The experimental results sections outlines used hyperparmeter selection in our experiments.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: We follow the standard approach in ATP literature to prompt the LLMs many times and report whether the proof generated by LLM has passed the formal verification system in any of those attempts. Repeating the prompts is the way that the community deals with statistical variability of LLMs because there are formal verification systems that can verify the correctness of outputs. The other method that ATP community deals with statistical variability is report the accuracy models given various number of attempts by the LLMs.. We have followed the standard methods in the ATP literature to report the variability of the accuracies: prompting the L.LMs many times, and reporting the accuracies for various numbers of proof attempts.
16

---

Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by enror bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report I-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information the puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
Computational resources used are stated in the paper.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics https: http///neuiip.p.eee
Answer: [Yes]
Justification: The paper closely follows the code of ethics and all generated/dowmloaded data has gone through sanity checks.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative socictal impacts of the work performed?
17

---

Answer: [NA]
Justification: The paper proposes a framework that reduces sampling overhead while im- proving accuracy of whole-proof generation models. The work does not explicitly address societal impacts.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, scraped datasets)?
Answer: [NA]
Justification: We do not foresee any issues arising from the release of our method that would require safeguards.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (c.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: All relevant datasets and models are referenced the paper and supplemental materials.
Guidelines:
18

---

The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should provided.
assets are released, the license, copyright information, and terms use in the package should be provided. For popular datasets, paperssi thcode. com/ com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: The method is described clearly in the paper. The code documented and will be released after acceptance.
Guidelines:
The answer NA means that the paper does release new assets.
Researchers should communicate the details the dataset/code/moodll as part their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: This work has no experiments that involve human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Question:
Answer: [NA]
19

---

Justification:
This work has no experiments that involve human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with
human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality the research, declaration is not required.
Answer: [Yes]
The method uses LLMs to produce formal proofs and they are further utilized by the proposed framework. We describe the use LLMs at every point of our framework.
Justification:
Guidelines:
The answer NA means that the method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy for what should or should be described.
20

---

A Additional implementation details
Algorithm ! presents a high-level pseudo code the Apollo framework. We highlight that the framework is built-upon the recursive function calls up to maximum recursion depth given by parameter r. LLM refers to a proof generator model that takes in a proof statement and outputs formal proof attempt.. Lean LommCerpiler refers Lean REPL that verifies the proof and outputs True or False. In the case False, also provides detailed list of errors, their locations and types along with the error messages generated by the Lean compiler. Other functions in the pseudo code (SyntaxRefiner Sorrifier, AutoSolver, ProofAssemblery represent the sub-modules described in the main text. To give deeper insight into Apollo's design, outline the rationale and responsibilities each core module.
A.1 Syntax Refiner
The Syntax Refiner class applies set of rule-based corrections eliminate syntax errors in LLM- generated Lean code. During model experimentation, we collected corpus of common mistakes, such as stray Lean keywords (from, begin... end), misplaced tactics, or missing delimiters, and encoded each repair as regular-expression rule. For example:
Convert [from by] to [: by].
Replace Lean 3 blocks (begin... end) with the corresponding Lean structure.
Ensure that commands like ru use correctly placed square brackets to avoid compilation errors.
In more complex cases, multiple regex patterns and replacements are composed to restore valid Lean 4 syntax without altering the logical content of the proof sketch.
A.2 Sorrifier
The Sorrifier module uses feedback loop between Apollo and the Lean REPL follows:
1. Apollo sends the current proof candidate to REPL.
2. The REPL returns a list of error messages and their source locations.
3. Apollo parses the proof into syntax tree, navigates to each failing sub-lemma, and attempts fix replace with sorry placeholder.
4. The updated proof re-submitted to REPL, and this cycle repeats until no error remain.
If the REPL indicates the original theorem statement itself is malformed (e.g. due LLM hallucina- tion), Apollo abandons the current proof and requests a fresh generation from LLM. One example of malformed formal statement is if LLM introduces a variable in hypothesis that was previously defined. Such case would trigger compilation error in the formal statement; therefore, when parsing the proof, Apollo will catch this and request fresh proof from LLM. To guarantee consistent variable types during lemma extraction and proof assembly, Apollo sets the following Lean options true:
set_ aet_option pp instanceTypes set_option pp. mpmemriiis true set_option pp. coercions. types true set_option pp.letVarTypes true set_option ap.structurelnnstacceyyees true
aet_opttion pp- ip-instanceTypes true pp.maars.vihhTpp. set_option coercions true set_option pp. funBinderTypes true set_option pp. piBinderTypes true
set_option pp.mvars. withType true
so that the compiler reports explicit types (e.g. Z vs. RR). This fail-safe prevents trivialization of theorems and ensures correct typing in the final assembled proof.
21

---

A.3 AutoSolver
The AutoSolver module takes the "sorrified" proof and applies sequence of tactics to close as many goals as possible:
1. Hint-based tactics. It first invokes hint, which proposes candidate tacties. We filter out any suggestions that merely progress the goal and retain only those that fully discharge it.
2. Built-in tactics. hint fails, AutoSolver systematically tries a suite of powerful Lean tactics, such as ml inariith, norm_num num, norm_ cast, ring_nf, simp, simp_all, and others, often combining them with try to catch failures without aborting.
3. Recursive fallback. Any goals that remain unsolved are reported back Apollo. Apollo queries the REPL for the exact goal statements, spawns corresponding sub-lemmas, and then invokes the full repair loop (LLM generation, Syntax Refiner, Sorrifier, and AutoSolver) each sub-lemma.
This tiered strategy maximizes automation while ensuring that challenging subgoals are handled via targeted recursion.
Algorithm 1 Apollo Pseudocode for Formal Theorem Proving
Require: problem statement ps, current recursion depth Yourrents maximum depth r
1: if Tourrent is not initialized then
2: Teurrent f-0 0
3: end if
4: if Tourrent > r then
5: return sorry
If recursion depth reached, return sorry
6: end if
7: proof LLM(ps)
Generate proof from LLM
8: proof + SyntaxRefiner(proof)
b Refine the proof syntax > Patch failing sub-lemmas
9: proof Sorrifter(proof]
10: proof= + AutoSolver(prouf)
> Try built-in Lean solvers
11: if LeanCompiler(proo))
True then
12: return proof
end if
14: Feurrent <- Teurrent +1
n + (ountSorricssprooff
b Number of "sorry" placeholders
16: sub_proofs + do
for
18: pSgnat + GetThooremGolliproooj
sub_ps- 4- TransformGool (p8
20: sub_proof [[]]] +- ppollo(sub_ps) Feurrent;
end for
22: repaired_ + ProofAssembler((ntb prooooffss
23: return repaired_ppood
B Discussion on maximum budget of @K and Apollo
To better highlight Apollo's contribution to token efficiency, we report token counts under two settings: (1) the budget over all attempted miniF2F-test problems, and (2) the budget restricted to proofs where Apollo was invoked. For instance, if the base LLM proves a theorem without Apollo's o assistance, its token usage included only in the first setting. In contrast, the base LLM cannot prove the theorem its own but succeeds with Apollo's help, its token usage is counted in the second setting. Results for setting (1) are shown in Table 5 while results for setting (2) appear in Table 6
We emphasize that, regardless of the token-count setting, Apollo consistently consumes fewer tokens while achieving higher accuracy, highlighting effectiveness. Throughout this work, we primarily report results under setting (2), as it more directly highlights Apollo's contribution: the reported token usage is not artificially reduced by problems that the base L.L. could solve independently. This makes Scenario (2) more representative measure of our contribution.
22

---

Table 5: Comparison of maximum/average sample/token budget across @ @K sampling and Apollo repair on the entire miniF2F-test dataset.
Max sample budget
Average sample budget
Max token budget
Average token budget
Model
Goedel-SFF
25600
9730
12.7M
4.8M
Goedel-SFTee -polll
1100
335
548K
167K
Kimina- 7B
1024
373
1.3M
1.6M
Kimina-7B+Aae AB+Apol
888
189
3.8M
818K
Table 6: Comparison of maximum/average sample/token budget across @K sampling the entire miniF2F-test dataset and Apollo repair exclusively on Apollo- problems.
Max
Average sample budget
Max token budget
Average token budget
Model
sample budget
Goedel-SFT
25600
9730
12.7M
4.8M
Spedel-SFF+Apolloo
1100
618
548K
307K
Kimina-78 7B
1024
373
1.3M
1.6M
Mumina-7B+Apoln
888
367
3.8M
1.6M
C Additional evaluation results
We also conducted experiments the ProofNet (9) dataset using the Preiiaa--eveeeeeee------ 7B model. Table summarizes the sample/token budget and accuracy. Incorporating the Apollo agent with Kimina not only improves accuracy by 7% but also reduces token consumption by 25%.
Moreover, we observe rising adoption of REPL-based repair, introduced in 44]. Currently, models such Goedel-Prover. V2 are fine-tuned REPL outputs paired with faulty Lean code, enabling the model to repair missing or incorrect proof fragments using this feedback. Following [44, we seneral-purpose compare Apollo against REPL-feedback baseline using the general purpose 03-mini model. Table presents the results: Apollo outperforms the REPL-feedback approach while requiring a smaller sample budget. We view REPL-bassd feedback complementary and expect it work well in conjunction with recursive, compiler-aided repair of Lean proofs.
Feedback prompt schema
This is incorrect proof:
[model's 's last proof]
Compilation errors follows:
[Lean's error messages]
Based this feedback, produce correct Lean code for the following problem:
[header]
[informal prefix]
[formal statement]
We also evaluated Apollo against the RMaxTS method proposed in 45 This approach employs Monte Carlo Tree Simulation explore the proof space and truncates the search whenever Lean compiler errors are encountered. RMaxTS has been shown to further improve the accuracy of whole-generation provers. For our evaluation, we used Kimina-Prover-PPevii Disttll-- as the base model. Table Apollo outperforms RMaxTS by 10.7%. These findings further reinforce the effectiveness of the agentic recursive repair approach.
9 reports the results. At comparable sample budget of approximately 2M tokens,
23

---

Table 7: Comparison of Apollo accuracy on the ProofNet dataset. generated tokens by L.M..
Token budget is computed over all
Method
Model size
Sample budget
Token budget
ProofNet
Simina-Preeiens
7B
128
559K
11.3%
Simina-Preview+AApllle
7B
415K
18.3%
Table 8: Comparison of Apollo accuracy against compiler (REPL) feedback based repair on the miniF2F-test dataset. Token budget is omitted since OpenAl API does not provide exact token budget with response.
Method
Sample budget
Accuracy
03-mini
1
3.3%
03-mini
32
24.6%
03-mini REPL feedback repair
5
17.2%
03-mini + REPL feedback repair
10
25.4%
03-mini Apollo
8
40.2%
D Computational resource considerations
Our emphasis reducing sample complexity is driven by resource allocation. CPU performance is not a limiting factor in our setup: the Lean kernel remains efficient even under high parallelization with proof verification typically completing in 6-200 seconds. To guard against inefficient structures, we impose a 5-minute compilation timeout, which is rarely approached in practice.
By contrast, GPU resources were the primary bottleneck. Running Kimina- Sereerr--eeeiee--iieeeeee on a single A5000 GPU with a 16,384-token context window takes 700-2,000 seconds per problem, over 11.5 minutes at @ 32 sampling. Increased sampling exacerbates this cost, and even with eight GPUs throughput remains difficult to scale. While Lean-based servers such as Kimina-server continue to improve verification efficiency through CPU parallelization, the growing overhead of sampling highlights the need to minimize LLM invocations alongside improving theorem-proving accuracy.
Table Comparison of Apollo accuracy against other sampling methods on the miniF2F-test dataset.
Token budget is computed over all generated tokens by LLM.
Method
Model size
Sample budget
Token budget
Accuracy
Kimina-Preett Preview
7B
1024
4.5M
70.8%
Kimina-Prees Preiaa--PreiieeMMaTTSS 45
7B
4 x 128
2.0M
64.3%
Momina-Previc++Apoole
7B
589
2.2M
75.0%
24

---

E Extension of ablation study
To further elaborate on the ablation results presented in the main text, we measured the number of relevant Apollo module calls during inference. The results are shown in Table 10 Specifically, we counted the number of invocations for each Apollo-assisted problem the miniF2F-test subset. The findings are consistent with the ablation study reported in the main text.
Table 10: Number of Apollo module triggers across different models
Model
Syntax Refiner
Auto Solver
LLM Re- Invokr
Goedel-SFT
0.0%
100.0%
100.0%
Kimina-7B
0.0%
100.0%
100.0%
03-mini 100.0%
100.0%
70.0%
04-mini 94.7%
100.0%
64.9%
An example of Apollo proof repair procedure
Figure showss a detailed run of the Apollo framework on mathd_ algebra_ First, the LLM generates an initial proof sketch, which fails to type-check in Lean. Apollo then applies its Syntax Refiner to correct simple errors (e.g. changing "from by" to ":= by") and to strip out all comment blocks. Next, the Sorrifier replaces each failing sub-lemma with sorry statement (six in this example). The AutoSolver module then attempts to discharge these sub-lemmas: it resolves four of them, leaving lemmas #5 and #6 unsolved. Apollo recurses on those two: each is passed again through LLM, Syntax Refiner, Sorrifier, and AutoSolvers After this single recursive iteration, all goals are closed. Finally, Apollo reassembles the full proof and returns it to the user.
This example illustrates Apollo's 's repair logic. In this case the proof was fixed in one iteration; more complex theorems may require deeper recursive repair.
25

---

APOLLO Framework
Sute Freef Lecenss
LEM APOLEO
Luttn mesodee
Figure 6: Step-by-step Apollo repair on mathd_algebre 3332 The initial proof and all sub-lemma proof's generated with o4-mini, then systematically repaired and reassembled by Apollo.
26

---

LLM
LLM APOLLO
Inport
inport
import herop
import Aesop
set sat_option sixteartbaatts
set option vaxtearibeats
open nigoperatora Real Net Togoloogy
open higoperatora Real KAt Topology Ret
theoren mathd, algebra_ 1in k N) (he Even
theores nathd nathd_ aagebddaagaaaaaa_e spollo N) (bo
(bi [(I x in ringet.range 8, * 112
Even a)
in Finset.raage
TCE is Finset.range k 71 in Finset.range 5, by
5::0
233
aimp_all
nf at
simp_all
eq
(Tk
53 by linsrith
have eq (5 (1a by
<Tk
have even (n N), a
linarith
even
N),
have two divides 53
(d 2),
exact even.existe two nsmall
[- even ]un] eq_aubet [eq_aubet]
have soo_dividex_a_ 53 :e by onega
2),
exact ((t5) (1n Tk.
have vid_ed
(d rintro <d, hd)
have dividee := by
a
1
riatro (d, bd)
by noen pam
have mod53 (53 2)
by
by norn_nun
have sod_d (2 d)
[hd] nw [mml_nod] at mod53
TW [hd] mod53
mH-Emmt-ndd
have contra False
limarith
apply div_diie exact two, divides_ss exact Falae. contra
contra
by
apply cot divides
exact tvo, divides_59
exact 7alue. alin contra
Figure 7: Proof attempt of mattd_aaaeeeee Btthhdd_agebbr_______ produced by the base model (o4-mini) versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
G Comparison between base proofs generated from LLMs and Apollo-repaired counterparts
In this section, we present and discuss examples of initial proof attempts alongside their Apollo- repaired counterparts.
Figures 7 8 illustrate cases where Apollo repairs the proof without invoking the LLM again. In each example, the LLM struggles to generate the precise tactics needed to close certain goals; however, we find that regenerating the entire proof is unnecessary. Instead, built-in Lean solvers can discharge those subgoals directly. Moreover, in Figure 7 problematic block #3 is resolved simply by removing it, since the surrounding proof context correct. Thus, omitting problematic lines can sometimes yield a valid proof.
In Figure 10 one goal is expanded via an LLM query, but the model injects tactics that trigger no goals to be solved error. Apollo then repairs the first block using a combination of L.LM generation and AutoSolver, while the second block is removed entirely.
Figure IT illustrates a case where the model fails to apply nl nlinarith th to discharge the goal. We observe that, when uncertain, the model often resorts to broad tacties in hopes of closing the goal. Here, the goal too complex for nl inarith, so Apollo leverages both the LLM and AutoSolver to guide the proof to completion.
Figure 12 illustrates an example of proof that required a recursion depth proof attempt. We observe that LLM's proof structure is correct; however, in many cases it over-relies on built-in solvers and rewrites. However, since the goals are too complex, this approach leads to total of nine error blocks. Repairing those blocks requires aid from both AutoSolver module of
to repair the initial
27

---

by Apollo and LLM itself. We show that if LLM grasps the correct approach, then Apollo is able to repair fine grained logic errors produce correct proof.
Figure 13 illustrates a case where the LLM produces an incomplete proof sketch. The first half of the proof is correct, but the model fails to discharge the remaining goal and instead uses all_goals positivity. Apollo detects this error and performs two additional recursive repair iterations to complete the proof.
Figure illustrates a case where the base model takes a lazy approach by trying to close all goals with linarith. In contrast, Apollo's repaired proof performs additional setup and discharges each goal by first proving the necessary auxiliary hypotheses. This example shows that, although the model often understands the high-level strategy, it lacks the fine- fine-grained tacties (and compiler feedback) needed to close subgoals. Apollo decomposes the proof, identifies the failure points, and applies targeted repairs generate fully verified solution.
Figure T5 shows another scenario in which Apollo successfully closes the first two blocks with linarith, but the final block requires deeper reasoning chain. Apollo augments the proof by introducing and proving the missing lemmas, which leads to a correct solution with a series of rewrites.
Figure presents an example of very large repair. As in Figure 12 Apollo requires r fully fix the proof. The final proof length increases from 100 lines to 216, which means Apollo applied roughly x2.2 more tactics to close the goal. The repair relied on combined effort from AutoSolver and the I.LM to close all goals. We show that, even for large, complex proofs, Apollo can repair each failing sub-block and generate a correct solution.
LLM
LLM APOLLO
import Pathlib
inport ib inport Aesop
import Aerop
set_option mxHeartbeate 0
set_aption zaHfeartbeats 0
open sigoperators Real Bat Topology Bat
сpez. sigoperators Beal Hat Zopolegy Mat
theores mathd algebra__at 141 31m (4 b
theores nathd algebra 141 ssl_apollo (a b R) (bs
180) (ha : (a
54)
180) (h: (a b
54)
2
have h3 : b by
have h3 1 b
field_sinp
limarith
have b4 (a b) 2 725 by
have h4 : (a b) < 729 by
[b9]
norn, pan
n01e, nux expand
expand :- by
:- by
have step1 4
729
:= by
have step1
725
[expaed, h4]
by
have step2 729
729 360 by
IW eexand,, hd] step2
[b,]
729 360
by
have 729 360 369
limarith
nore_ pun
atap3 729 350
exect stepl. (step2, step3)
linarith
Figure 8: Proof attempt of mathd_ mathd_algebra 141 produced by the base model (o4-mini) versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
28

---

LLM
LLM + APOLLO
Import
import import Aesop
import hezop
sat_option: nixtiaar cbouta
set option musticaribeata
higoperators Resl Bat Togology
1i Rigoperatork Real
Mat Togo logeloggy Ret
theoren
ba
apollo
A 0 < e) (br ceco E) (he 1 b a
0 < chbhb c) (hn
bJ (la
* (b
(o
A (b
(c by
mlimarith [og_nonnng (a b), ng_nonnng (b o), sq_nonee a), sq_sonneg nonoen e), mouneg a),
mlimarith [erg_nonne (a b), eg_nonneg (b o), "c_oonn a),
mul pos (oub pos. hi)
pal_pos le.left te.hiiht.loft,
(sub ssub_pos.upp hz), mal_pos
sul_pos be.left w..rght.rightt pos_pos hightttt.left hg.right.
(sub_pos.upp .up hu)
(wab_pox.app upe he). mal_pos (wab_pox.nps hy (sub_pos. h.)]
Figure 9: Proof attempt of imo 1983_p6 produced by the base model Ceamina-Prover-Peee Distill-7B) versus after Apollo's 's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
LLM
LLM + APOLLO
import Kathlib
inport Mathlib
import
inport
saxPeartbeate
zasfeartbeata
sigoperstors Real Topology
sig0perators Zopelogy
induction_pordageee powpspppeppsspooottttn...a.
induction induction_pordippeee www.pppptsspppeettttsseeeeaeeee
(hg n) : inducticn mere =>
N) (he <.K))
by sero contradiction sucz +>
succ he casea
with
norn,
nore, nure induction with zero
simp all [Finset.prod coc_sd_o______ooooooo sop
Mat Nat.cantt_scce pscc, div_et_nol_ine]
noen nuw
Priaset.pro. Ice suce succ_topp] at ha bo <i> linarith ih
sing_nf linarith
cases with
nore, nun
[Pinset.prod_Ieet Secd__To___ee_tggeeeeeeee [op]
<p>
suce =>
simp
[Fiaset. prod_roeeeeeeeeeee succ top, pou_s mal_comn]
succ
simp_si
[Fineet.proo pettret-roo__ee_seeee Serro__oo_suc__teee top, Nat.costt_uceee
div_ec_ml_inr]
zing.nf
länarith
Figure 10: Proof attempt of pwr.iiiooooodddooopprprooo
produced by the base model (Goedel-Prover-SFe) versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
29

---

LLM
LLM APOLLO
Inport
inport import Aesop
import žеtoр
set sat_option. scsBeartbaata
set_ option vaxtcaribeats
sigoperatora Real Nat Togology Rat
open bigoperatora Real Kat Topology Ret.
theores mathd_at Bealid___ebb______ _______________
(HReell
theores nathd_ale beaehdaaagebaa.__e 293 sapolll 883es1)
Real. Real.ngrt (50 x) Real.egrt (12 x) Real.agrt
Real.egrt (60 x) Resl.agrt (12 Real.egrt
Real.ogrt (35
zu [e- Real.sert mal (by positivity),
by
Reall seal..grt_mmn poaltivity)]
Real. paal...rt_.maa positivityy) seal.sqrt_maa (by positivity):
xing_nt
[eeal.agrt__ee ____e_______________________ sell__eeee
sing_ef
ring_nÉ
su [Real.agrs__eq ring_nf nomm have b (V(X R) v25)*2 R) by [HO2_poN]
simp
zv [b] xing
simp simp_all only [offlat_poo pos,
ma1, Lonnnnnngggg. of__p_fo__g__hheeee__eee Nereel
pow, jow_nomeeg]
exact =000 10 have
VCC
(36 R) by simp_all only
zero
rXResl. zero_ la______________ooo____________c agrt agrt_mal, mal, oftfat_pos,
noo_nonneg__ie cicii_of__o_________ right,
Real.sgrt_ppo Real. egrt, pogrt_nnneg]
have
R) have B <[(x R) 35) sert nonneg 35)
coe nonseg
have (0 36 Nun
mul (mal_nomne)
Figure 11: Proof attempt of mathd_ algebraa 293 produced the base model (Goedel-Prover-SFTT) versus after Apollo's 's targeted repair. The left shows the original end-to-end LLM output, which does compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
30

---

LLM
EE0O ANOUOO
carsyae tr singast bry SUNLLE
TeyLogy
Pepoogg
lane 337 b co 20P
sing al only
stop enty Cond tree,
beer
to prit
taxe
CAART CEAL HLLLLLL 1113 XSSa 111
lewe
Kllea))
(eled)))
Sinarill
at
Save
sing way (KKiLIORs, MUN
AACHCTORNNIIIIAE ARL PLMM
spact
tr
here ba Oo wearl (snel sot suat
stoy al eleg
Palliegi:: C2
ZIGGLAND
Lieeciss
Lone SiR
to
car
DE Bay 1031
Coosal:
slagal
salay
Figure 12: Proof attempt of bathd_algebrre 184 produced by the base model Ekimina-Proves Preview-Distill-7Bt versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
31

---

LIM
Jeport HALROAD
LLM APOLLO
Jeport
spea Rigogacntock DHE sepRingy Bat
tave VEER
tapacogy
sheorm mosnd Aigebon Si0 (a PROAA))
S0al- ages Cco 2002 apy (12
VEAD via R3
DOLL aQES 200L REES PAA2-AG
Mall.ages
hare sea2-agrs (90
(000
real. weal- aqes (100
lave viaaa
mallapprusz panlisntop))
seal Aari.. (by poststricy))
zn [35] have
bace hert <Cass R1 v130
[hs)
stoguat
<>> shap [x
<z> atmp [x
Steartch [aw Crom by
pontsionay)
[ha]
2M [eaal, aar (by pontcinccp1]
slaguall tey stegunt
deside
[eeat-xeurtrr Oy aserssen]
2v [aast, suct_re thy stop [x])]
Lisurich try alimaries
[hess]
[eeal.ngrT_mn))
<> ciegust
<in rlng
[h24]
(12 VELS 453 R3
<.n ciegust
VETx R) <1x 80 CAD 81
Minerith [n23]
sze ciegued
ev (+ hR)
ctop
<Tx 82
baee 141 v K2 <1
beve Th
[h4s,
Stearsth
[hi,
stop sanne]
sxre,
sing_all
ving.st
Figure 13: Proof attempt of mathd_ mathd_algebra algebra__a22 293 produced by the base model "Kimina-Prover Preview-Distill-7BB versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
32

---

1LM
EER ANOUO
Aaliit
it
mnaatti aesnciiciio the
Let Licae Resanccceee taee
sogLAl moy (nA
to A Ge D
slottra perr touern, dorwert petoratwaaes Pepert sue
Kloatre terrlnsere doteeets strpeet fagera
thy oe CI to
Do
canes comy morel,
512
cags
Lave
siggat
eqatioe
1942
hare
tE Q C (
Ct + in
tare K 0000000000000 649
por
Kxtipt Q C1. O
DIRLAT
CALAE
MLAARRCEEI (3) 13 CH
ERRLASE FORLIC 1or MiniEAn
MODL UF
TEE Linectss TEF SlOWEIC
131
(C-48
Figure 14: Proof attempt of algebra__ iwarlineeree__p3ae 2ttr111.mmmmmmmeeee__8ffef 1_e produced by the base model (o4-mini) versus after Apollo's 's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
33

---

LIM
LLM ATOLLO
Aepart MALASER
ARport MALKEAD
Dapacogy
spe
Vieccm MHSSON piR,Aie RJ (o.
tiewres M0A22A 2010 ppt. CA 8) (1e
Lave los 2oob.Jog (14
zask.log
ConaL-ing Log CE 200..cog
seal, Log
663
Ang 21 anac.cog
ciecce 221 stop
co (bom]
cinsee
Hield Aiald_aiop [sen).log,_d 2og,ail cnal inl..ieg.int.
saal Log 534] as be
cieccs 221
have la
stop
Lisactch
riats_xtmp (weal: Jeguei
seall Ltg..ie......................... seal 1og,29d
have bar_prod
tha]
[r_sseance]
leal.log_570
ciegust
Let leab:log
tave '_Jossees 1 by 2_ Bealing
have
Beal (Rea)
ne [mXee])log log.lll 2_30000co y_
Ln by stmp_al1 only [ec,ec dir, 1sg_re_009, talns,ee 1og_neg_ 20g ssg_
[BA3]
offer (e,eflee)
beee 36 6 beal-log (t 1o teel.log
(t. beal exp 20p0) by heve 7.rt,
snect
step_al All only (ec_ee: if reco.
and www.__eeeeeeeereeeeeee 13*2 DX 10 ee (MAY') 410E,4
sst_fxlae_vec
phaV_prod) 45C2,40
Figure 15: Proof attempt of amc12a_ amc12a_2019_______ __11_11________ produced by the base model Sroedee-Prover-FFF versus after Apollo's 's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals.
34

---

121 APOLLO
Mance HO Www.oiil Mo L.r.
May SAT SIA
une 14
love
bave
Herrity
ALl sancune veraem
have Relm
stegatt stecal
Lune
Juno ASE
stoy Diis
bave 1a0
Lawe
mos stegatt Jestde
stay Dakiidd
bace 24 (VA))
rass Sod
Figure 16: Proof attempt of mathd_ mathd_ algebra_ __9 produced by the base model (Kimina-Prove Prover- Preview-Distill-IB) versus after Apollo's targeted repair. The left shows the original end-to-end LLM output, which does not compile in Lean; the right shows the corrected, repaired proof assembled by Apollo that closes all of the goals. Import headers are the same as other presented examples, for visibility they were omitted in this diagram.
35


Reviews:
[{"review_id": "N8BZdNuxJ6", "reviewer": "Reviewer_hqN5", "summary": "The paper introduces Apollo, an automated modular pipeline that enhances large language model (LLM)-based theorem proving by integrating LLM outputs with feedback from the formal verification system (Lean4). Rather than naive resampling, Apollo iteratively identifies and repairs errors in LLM-generated proofs through a sequence of specialized modules. Specifically, the pipeline includes a Syntax Refiner that corrects superficial syntax issues; a module that replaces faulty sub-proofs with Lean's proof placeholders; an Auto Solver that applies built-in tactics to resolve sub-goals; and a recursive repair mechanism that re-invokes the LLM on remaining goals using Lean's feedback. Finally, the Proof Assembler re-integrates the repaired components and verifies the complete proof. The proposed method demonstrates strong empirical performance on the miniF2F benchmark across different base models.", "questions": "1) For a more rigorous evaluation, I suggest fixing the base model and comparing Apollo with alternative strategies under the same sampling budget. In particular, using the number of tokens as the budget unit rather than the number of sampled completions, would more accurately reflect computational cost. Additionally, evaluating the method on a broader set of benchmarks would help demonstrate the generalizability of the approach.\n2) The core idea of identifying erroneous segments and selectively repairing them is conceptually straightforward. The contribution primarily lies in the agentic system design and modular workflow. Clarifying how Apollo differs from standard modular repair workflows or existing agentic frameworks would help assess its conceptual contribution.\n3) The paper would benefit from a direct comparison with standard depth-first or best-first search strategies. In tree search, invalid branches are pruned early, potentially reducing token usage by avoiding downstream propagation of errors. In contrast, Apollo must retrospectively correct affected steps, which could be less efficient.\n4) The descriptions of Apollo's modules suggest that they are LLM-based agents, but no prompt templates or examples are provided. Upon reviewing the source code, it appears that the modules are rule-based programs. If so, this raises concerns about scalability and generalizability: manually crafting rules for different failure modes is unlikely to scale across programming languages (e.g., from Lean to Prolog, even across different Lean versions), different LLMs (some correction rules are model-specific according to the code comments), or datasets. Clarifying this aspect and discussing its limitations would strengthen the paper.\n5) Several components necessary for reproducibility are missing from the released source code, including a README, installation requirements, and datasets or download instructions.", "limitations": "yes", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\nThe paper is well-organized and easy to follow. The proposed method achieves strong performance on miniF2F benchmark with reduced sampling. The results analysis is thorough. The agentic pipeline is practical and aligns with human-like proof workflows.\n\nWeaknesses:\nComparisons lack consistency in model and token budget; more datasets are needed. The method focuses on workflow design rather than algorithm or architecture-level innovation. No comparison with standard depth-first or best-first search methods. Modules rely on hand-crafted rules, limiting generalizability. Key artifacts (README, requirements, data) are missing from the code release.", "was_revised": true, "final_justification": "The authors improved the quality of their work by adding additional explanation. Although not too impressive, the work shows some improvement relative to baselines. As such I had increased my initial rating by one.", "rebuttal": "We would like to thank Reviewer hqN5 for the constructive feedback and suggestions on our work. The following is our response to the reviewer’s comments and questions.\n\n### **1. Reporting token budget vs accuracy across the board.**\n\n> Comparisons lack consistency in model and token budget; more datasets are needed.\n\nAs per your suggestion we are now presenting both generated sample counts together with generated tokens in all of our experiments across the board. In all the subsequent results, you will see comparison of tokens and accuracies for all of our findings except for o-series models. Across the board, for all LLMs, Apollo increases the accuracy while reducing the token count. We believe this addresses the first item under the weaknesses in your review. Thank you for this helpful suggestion which highlights the contribution of our work much clearer.\n\nTable 1: Performance of base Kimina-7B against LLM with Apollo on ProofNet dataset\n| method        | budget (highest sample count) | budget (tokens) | accuracy |\n|---------------|-------------------------------|-----------------|----------|\n| Kimina-7B        |                           128 | 559K            |   11.30% |\n| Kimina-7B+apollo |                            96 | 415K            |   18.30% |\n\nTable 2: Performance of base Kimina-7B against LLM with Apollo on PutnamBench dataset\n| method        | budget (highest sample count) | budget (tokens) | accuracy |\n|---------------|-------------------------------|-----------------|----------|\n| Kimina-7B        |                            32 | 180K            |        7 |\n| Kimina-7B        |                           192 | 1.1M            |       10 |\n| Kimina-7B+apollo |                           108 | 579K            |       11 |\n\nWe observe that applying Apollo improves the accuracy across both benchmarks while reducing the number of generated tokens compared to the base LLM.\n\n### **2. Limited generalizability**\n\n> Modules rely on hand-crafted rules, limiting generalizability.\n\n**We have now experimented with the Goedel Prover v2 8B model, the latest state-of-the-art theorem prover released in July and Apollo increases its accuracy by 1.6% while reducing the token budget.** Although this model was released two months after our method, our results demonstrate that Apollo can still enhance existing provers’ accuracy, highlighting the framework’s longevity and generalizability.\n\nIt is also notable that two of the best models in the literature, Goedel Prover V2 and Kimina Prover have now added modules for error fixing using the list of errors generated by the Lean compiler. This is an indication of the trajectory of research in the community and the level of interest in adopting methods such as Apollo.\n\nApollo is an agent that combines rules, LLMs, and built-in solvers to produce correct proofs. We acknowledge that some components, like the Syntax Refiner, which uses fixed rules to correct syntax mistakes, may become outdated as general-purpose models improve and stop making those mistakes. However, Apollo is fully modular and its modules can be added, altered, or removed, and possibly extended to new languages and use cases. LLMs can be swapped via a configuration file, and built-in solvers will continue to improve. Apollo does not depend on a specific Lean version (we tested v4.9.0 through v4.17.0), so upgrading individual components can yield better performance. \n\nTo ensure generalizability, Apollo encodes code into an execution tree based on indentation and a few Lean-specific rules. Any language that uses indentation for code blocks could be supported with minimal overhead. The framework is designed to be modular and extensible: any module is replaceable and scalable.\n\n\n### **3. Comparing Apollo to alternative sampling strategies.**\n\n> No comparison with standard depth-first or best-first search methods.\n\nPer your suggestion, we compare Apollo against RMaxTS [30], using the Kimina-Preview-Distill-7B model as the base. RMaxTS employs Monte Carlo Tree Search to explore the search space progressively, leveraging an “expand and truncate” strategy to adapt it for use with whole-proof-generation models.\n\nTable 3: Comparing Apollo to RMaxTS sampling strategy\n| method        | max sample count | tokens | accuracy |\n|---------------|---------------------------|-----------------|----------|\n| Kimina-7B        |             32            |       140K      |   63.1%  |\n| Kimina-7B        |            1024           |       4.5M      |   70.8%  |\n| Kimina-7B+RMaxTS |          4 x 128          |       2.0M      |   64.3%  |\n| Kimina-7B+Apollo |            589            |       2.2M      |   75.0%  |\n\nPer your request, we present Apollo’s maximum token expense to illustrate its efficiency in the worst-case scenario. As shown in Table 3, LLM with RMaxTS achieves 64.3%, while Apollo pushes the accuracy further to 75.0%, with 10% more tokens in the worst case generation scenario. Although Apollo’s worst-case budget slightly exceeds RMaxTS, its average budget is substantially lower. Apollo generated 307 proof attempts and 1.3M tokens on average.\n\n### **4. Contribution of agentic Apollo framework**\n\n> Clarifying how Apollo differs from standard modular repair workflows or existing agentic frameworks would help assess its conceptual contribution.\n\nAlthough agentic workflow has an extensive and successful use in the general LLM literature, it has not been widely adopted in the ATP pipelines. We are now adding additional discussion and comparison with that literature outside the ATP to address this comment.\n\nAgentic LLM systems have long incorporated external tools, such as symbolic engines, APIs, search access, and memory modules, to improve performance and reduce hallucinations [1]. Recent multi-agent frameworks often focus on advanced inter-tool interactions [2] and complex agent-to-agent interactions [3], but the core insight remains: teaching LLMs to integrate outside resources is key. The outside source in our approach is the formal verification system: Lean. In most applications of agentic LLMs, there is no formal verification system that can automatically identify the errors in the output of an LLM. In ATP, however, we have the Lean compiler which automatically provides the least of errors, their exact locations in the code, and some descriptions about the errors. Hence, we try to leverage the Lean compiler as much as possible in our agentic approach. Like most agentic approaches in the LLM literature, Apollo also takes inspiration from the workflow of humans, in this case, how mathematicians work: break the proof into parts, simplify each piece, and iteratively rebuild until no goals remain. Apollo automates this process by developing a module to perform each of the operations and centers on a single, powerful tool: the Lean language and its built-in solvers. Such design bridges the gap between LLM-driven proof generation and automatic theorem provers.\n\n### **5. Using tree search strategies for token budget reduction**\n\nWe thank the reviewer for the insightful suggestion of using search methods to further enhance the efficiency of the proposed framework. If we could assign a likelihood to each decomposed sub-lemma’s difficulty/correctness, using tree search methods could result in reduction of tokens with no accuracy changes for Apollo. In other words, such a strategy may further reduce the number of tokens used by Apollo without changing the ultimate accuracy we have reported in the paper. Consider a scenario with the three “sorry” statements in a theorem. Indeed, if the first “sorry” is particularly challenging, DF or BF search strategies could reduce token usage by pruning dependent sub-blocks early. In tightly constrained GPU settings, where we solve sub-goals sequentially, this might lower overall token counts. However, our current design emphasizes parallel computation across multiple GPUs, so Apollo tackles all three “sorry” statements simultaneously. This approach may increase the number of generation attempts and total tokens generated, but it yields faster inference when we have three free GPUs that we can utilize in parallel. It’s a system-design tradeoff, and we agree that in single-GPU environments, one could introduce additional search heuristics to guide recursion more intelligently and further reduce token budgets. It could be an interesting future direction for agentic repair systems like Apollo.\n\n### **6. Additional reproducibility components**\n\nWe appreciate the reviewer’s attention to reproducibility. The current demo release was intended to illustrate the core framework rather than serve as the final toolkit. In the full code release, we will include a comprehensive README, a detailed list of installation requirements, prompt templates, and clear instructions or scripts for downloading and preparing all datasets.\n\n---\n\nWe made a significant effort to perform additional experiments and address your feedback. Computing the token budgets demonstrated the advantage of Apollo across the board increasing accuracing and cutting the token counts. We also experimented on new models (Goedel Prover v2) and new datasets (ProofNet and Putnam Bench). Moreover, we made comparisons with MCTS, again demonstrating an advantage. Our paper and its contribution is much clearer as a result. In light of these improvements, we would appreciate it if you consider raising your score. Do you have any remaining questions or concerns?\n\n---\n\n[1] Taicheng Guo, et al. (2024). Large Language Model Based Multi-agents: A Survey of Progress and Challenges. ĲCAI.\n\n[2] Junde Wu, et al. (2025). Agentic Reasoning: A Streamlined Framework for Enhancing LLM Reasoning with Agentic Tools.\n\n[3] Chen Qian, et al. (2025). Scaling Large Language Model-based Multi-Agent Collaboration. ICLR"}, {"review_id": "DL9tjd9uHT", "reviewer": "Reviewer_KutC", "summary": "The paper proposes an inference-time workflow for theorem proving with large language models (LLMs) in Lean, which comprises a series of specialized tools that fix up common syntax errors in LLM-generated code, remove parts with errors, apply a suite of Lean's standard proof automation tools and otherwise recurse by extracting the remaining proof gaps as standalone proving problems for the LLM.\n\nCompared to the baseline of $k$ independent samples from the prover LLM, this post-processing and recursive repair significantly reduces cost / outperforms the baseline on the standard MiniF2F benchmark when comparing at the same amount of LLM calls. The method can be applied to any prover model and is both used with Lean-finetuned models like Goedel-Prover and general-purpose reasoning models such as o3-mini.", "questions": "see weaknesses 1-3: comparison to agentic setup? CPU times? ablations?", "limitations": "yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "**Strengths:**\n1. The post-processing and recursive repair appear extremely efficient at catching and fixing minor mistakes in the code, producing strong evaluation numbers on a variety of models.\n2. The different post-processing stages are clearly described and the paper is easy to understand.\n\n**Weaknesses:**\n1. The method is not compared against other inference-time methods such as putting the model into a multi-turn agentic loop where it reads in error messages and can decide freely how to solve the issue (by replacing a block, using automation tools, reworking a line etc). I understand that this is in part due to the fact that whole-proof generation models such as Goedel-Prover are not able to follow such instructions, but o3-mini and o4-mini certainly could.\n2. The comparison based on LLM calls is fair as long as GPU compute is the primary limiting factor. Given that in Lean proving setups, CPU execution is an increasingly important bottleneck, it would be important to see Lean execution runtimes, too, for getting the full picture.\n3. There are no ablations on the different parts of the post-processing pipeline. At least, it would be useful to see average numbers on how often which tool triggers with which model. I would be surprised, for instance, if the Syntax Refiner often triggers for the Lean4-specific models. Moreover: How many gaps can be solved with the Lean automation? How many recursive calls are being issued on average? (Table 1 lists the average total number of calls per problem but doesn't state from how many independent attempts these stem.)\n4. The method proposes ad-hoc fixes to rather superficial problems of current LLMs for Lean (confusion between Lean 3 and Lean 4 among general-purpose models; incomplete knowledge of all automation tactics), it is conceivable that the method will not be relevant for a very long time.", "was_revised": true, "final_justification": "Following the discussion, I increase my Significance rating (there is no careful analysis on agentic harnesses for Lean) and decrease my  Quality rating (important considerations and their interactions are under-explored, the comparison should include iterative instead of recursive repair, ablate LLM repair and rule-based repair separately and report early stopping numbers for the pass@k baseline just like for the repair methods). I still marginally recommend the paper given that it opens up these questions and provides valuable insights from the available datapoints already.", "rebuttal": "We would like to thank Reviewer KutC for the constructive feedback and suggestions on our work. The following is our response to the reviewer’s comments and questions.\n\n### **1. Apollo against iterative feedback repair**\n\nIndeed, iterative repair frameworks have proven successful and are widely adopted in the code-repair community. To evaluate how Apollo compares, we conducted a simple experiment using o3-mini as the base model. Over up to ten iterations, the model takes the incorrect proof along with feedback from the Lean compiler as an input and produces a corrected proof. Our findings are detailed below:\n\nTable 1: Comparing feedback repair to Apollo repair with o3-mini as the base model\n| method                    | budget | accuracy |\n|---------------------------|--------|----------|\n| o3-mini                   |      1 |    3.3% |\n| o3-mini                   |     32 |   24.6% |\n| o3-mini + feedback repair |      5 |   17.2% |\n| o3-mini + feedback repair |     10 |   25.4% |\n| o3-mini + Apollo          |     ~8 |   40.2% |\n\nFeedback prompt schema:\n```\nThis is an incorrect proof:\n[model’s last proof]\nCompilation errors are as follows:\n[Lean’s error messages]\nBased on this feedback, produce a correct raw Lean code for the following problem:\n[header]\n[informal prefix]\n[formal statement]\n```\nTo the best of our knowledge, there is no reliable method to obtain reasoning tokens via API for o-series models, so we report the results based on average pass parameters. We observe that Apollo outperforms this method with a lower average budget.\n\n### **2. CPU and GPU bottlenecks in theorem proving**\n\nIndeed, our focus on cutting the generated sample complexity is motivated by our observations of resource allocation. In our setup, CPU is not a limiting factor. Even with high parallelization, the Lean kernel is efficient and proof verification is fast. Moreover, to avoid verifying proofs with too many recursive calls and inefficient structures, we set a 5 minute limit on compilation. From what we have seen, compilers rarely get close to exhausting the time limit and on average proof verification takes between 6-200 seconds depending on its complexity.\n\nBy contrast, GPU resources are a substantial bottleneck in our environment. Running Kimina-Prover-Preview-Distill-7B on a single A5000 GPU with a 16,384-token context window takes 700 to 2,000 seconds per problem, over 11.5 minutes for @32 sampling. Increasing sampling cost makes this bottleneck worse. Even with eight GPUs and parallel generation, throughput remains slow and difficult to scale. Therefore, we focused not only on improving theorem-proving accuracy but also on minimizing the number of LLM invocations.\n\nWe also note that Lean-based servers are becoming more efficient. Kimina-server enables parallelization across CPU cores and accelerates proof verification. Going forward, we believe that increasing sampling costs will impose greater overhead on GPUs than on CPUs.\n\nWe will include this discussion in the revised manuscript.\n\n### **3. Additional information on connection between sampling costs and recursive calls**\n\nTo further clarify the connection between recursive calls and sampling costs, we present the following tables that reports the recursive calls, sampling costs and token usage for Goedel-Prover-SFT (goedel-sft) and Kimina-Prover-Preview-Distill-7B (kimina-7b). These results are an extension of Table 1 (main text) and they show connection between sample budget and recursion depth.\n\nTable 1: Relationship between $r$, sampling budget and token count on Kimina-Prover-Preview-Distill-7B.\n| rec depth     |    0 |    2 |    4 |    6 |\n|---------------|-----:|-----:|-----:|-----:|\n| sample budget |   32 |   96 |  191 |  307 |\n| token count   | 140K | 406K | 816K | 1.3M |\n\n\nTable 2: Relationship between $r$, sampling budget and token count on Goedel-SFT.\n| rec depth     |     0 |     2 |     4 |    6 |\n|---------------|------:|------:|------:|-----:|\n| sample budget |    32 |    80 |   151 |  362 |\n| token count   | 16.1K | 38.3K | 74.6K | 179K |\n\n### **4. Ablation studies**\n\nWe thank the reviewer for the comment on ablating the different parts of the pipeline. We performed ablation using two baselines: o4-mini and Kimina-Prover-Preview-Distill-7B. Below is the ablation study and each module’s contribution. The starting point is @32 for Kimina and @1 for o4-mini. Recursive repair is up to $r=6$ for Kimina and $r=4$ for o4-mini, while recursive repair for “base+SR+Auto Solver” case is $r=1$, since without invoking LLM Solver the sub-goals cannot be expanded and decomposed further. Results are shown in Table 3.\n\nTable 3: Ablation study of different parts of Apollo on o4-mini (general purpose model) and Kimina-Prover-Preview-Distill-7B (theorem prover model)\n| module                   | o4-mini | kimina-7b |\n|--------------------------|---------|-----------|\n| base                     |    7.0% |     63.1% |\n| base+Syntax Refiner (SR) |    7.4% |     63.1% |\n| base+Auto Solver         |    7.0% |     63.5% |\n| base+SR+Auto Solver      |   20.5% |     63.5% |\n| base+LLM Solver          |    8.2% |     69.3% |\n| base+SR+LLM Solver       |   18.9% |     69.3% |\n| base+Apollo              |   46.7% |     75.0% |\n\nFor general-purpose models like o4-mini, the Auto Solver delivers substantial benefits: these models rarely invoke built-in solvers and instead attempt to prove simpler goals manually, often resulting in hallucinations and redundancy. Applying the LLM Solver alone yields lower performance. Syntax Repair by itself fixes only one problem, but it’s critical for enabling other modules, without it, o4-mini shows little improvement. Although we expect the Syntax Refiner to become obsolete soon, we include it in the pipeline to support experiments with general-purpose models.\n\nBy contrast, Kimina-Prover follows a different pattern. The Syntax Refiner has no impact, this model is fine-tuned to produce only syntactically valid proofs. Auto Solver alone aids only one theorem, while repeated LLM Solver invocations yield a 6% improvement. We see a substantial performance boost when both modules are combined. Upon inspecting Apollo’s outputs, we find that the model often makes minor errors while preserving the correct proof skeleton, and many sub-goals can then be discharged with built-in tactics. Thus, the interaction of both modules produces significant accuracy gains.\n\nTo further investigate each module, we conducted a simple test to see how many times each module was called during an inference.\n\nTable 4: Number of Apollo module triggers across different models\n| model      | Syntax Refiner | Auto Solver | LLM Solver |\n|------------|----------------|-------------|------------|\n| goedel-sft |           0.0% |      100.0% |     100.0% |\n| kimina-7b  |           0.0% |      100.0% |      95.2% |\n| o3-mini    |         100.0% |      100.0% |      70.0% |\n| o4-mini    |          94.7% |      100.0% |      64.9% |\n\nAcross all experiments, the Auto Solver is always invoked to apply Lean solvers to each sub-goal; if it fails, it leaves the goal open and passes it to the LLM Solver. Conversely, the LLM Solver is sometimes bypassed when the Auto Solver discharges a goal without calling external provers. For Goedel-SFT and Kimina-Prover, the Syntax Refiner is never invoked. We evaluate only those problems proved with Apollo’s assistance. Note that the Sorrifier and Proof Assembler are always invoked, they decompose proof code and reassemble it, so they are omitted from Table 4.\n\nWe will include these results in the revised manuscript to emphasize the significance of each part of the pipeline and how they affect the overall performance of the framework.\n\n### **5. Relevance of recursive repair**\n\nWe agree that the relevance of Syntax Refiner is short-lived and it depends on how long it will take for general-purpose models to see enough Lean4 data. However, other parts of the pipeline are meant to be modular and upgradeable. We are not tied to any specific LLM or Lean version. Going into the future, Apollo will get better with the introduction of new LLMs and built-in solvers in Lean.\n\nMoreover, the current research trajectory indicates that leveraging the Lean compiler is a powerful idea already gaining traction in developers of models like Kimina-Prover-72B [1] and Goedel-V2 [2]. Both of these models include “error correction” modules that use REPL feedback to fix proof mistakes and were released two months after the proposal of Apollo. We expect researchers will increasingly integrate Lean feedback into LLMs to boost performance and reduce hallucinations. Apollo represents a step toward agents that not only generate proofs with LLMs but also incorporate external tools and resources, strengthening performance while reducing sole reliance on ATPs.\n\nTo further demonstrate the relevance of our approach, we conducted an Apollo repair on the state-of-the-art prover: Goedel-V2. Our preliminary results indicate that Apollo aided in solving four additional problems in the miniF2F-test, resulting in a _1.6% performance gain_. This model was released much later than our proposed method, and our results show that we can further improve the accuracy of existing provers, indicating the longevity of the proposed framework.\n\n---\n\nThank you once more for your insightful feedback. We’ve carried out additional experiments and incorporated your suggestions to strengthen our work. Given these enhancements, we kindly ask you to consider revising your score. Please let us know if you have any further questions or concerns.\n\n---\n\n[1] Haiming Wang, et al. (2025). Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models.\n\n[2] Yong Lin, et al. (2025). Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date."}, {"review_id": "vKZh1DU7JW", "reviewer": "Reviewer_gYTQ", "summary": "The paper proposes APOLLO, a modular, agentic pipeline that incorporates signals from lean compiler with LLM prover to achieve better performance in mathematical theorem proving. The proposed system includes a set of agents to analyze the proofs, fix the syntax errors, identify the mistakes, decompose failing lemmas and utilize automated solvers to boost the success rate of the whole proofs generated by an LLM prover. With APOLLO, the authors achieve 75% accuracy on miniF2F test set and at the same time improve the LLM prover’s sample complexity. They also demonstrate its wide applicability to general-purpose reasoning models such as o3 and o4.", "questions": "I will update the score if the authors address some/all the weakness points I listed in the last section. Additionally, I have the following questions.\n\n1.\tIn Fig. 3, the curve for APOLLO is cutoff at a relatively low sample budget. It’s important to understand how the accuracy scales with larger sample budge. Does APOLLO continue to prove more theorems or does it plateau and thus cannot further improve much more than the base model.\n\n2.\tIn Fig. 4, is the data included in the figure conditioned on the proof being correct? I think it only makes sense if the authors show the results on correct proofs only. Making the wrong proofs longer is not interesting or important.\n\n3.\tHow does the hyperparameter r transfer to sample budget? I suggest including a plot showing the relationship between r and sample budget.\n\n4.\tIs it possible to do pass@N on top of APOLLO? Is there a tradeoff between increasing r and increasing passes?", "limitations": "The authors have included a limitations section in the appendix. I agree that not considering step-level LLM prover is a main limitation of the work.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 2, "strengths_and_weaknesses": "The paper is well written, and the authors have shown a good amount of improvement with their proposed APOLLO. However, there is still space to improve:\n\n1.\tThe authors claim that they achieve state-of-the-art accuracy, but Deepseek-prover-V2-7B has an accuracy of 82%. I suggest the authors include this reference.\n\n2.\tI am not sure if the comparison of sampling budget is fair. Based on my understanding, the mean number of samples for APOLLO is computed as the number of function calls until it successfully proves the theorem or reaches a maximum recursion depth. Then to make fair comparison, I think for pass@k, the authors should also report the mean of number of samples until it FIRST samples a correct proof. I believe this number will be lower than the sample budget reported in the table.\n\n3.\tThe proposed method APOLLO acts like a search tree. As a result, it may be important to include comparisons with tree-search methods such as Monte Carlo Tree Search and check how much APOLLO improves over those tree-search methods.", "was_revised": true, "final_justification": "The paper was unclear about how they compare against the baseline. The authors has clarified this main concern. Given the fact that the authors have addressed most of my concerns, I increase my score to 5 and suggest for acceptance.", "rebuttal": "We would like to thank Reviewer gYTQ for the constructive feedback and suggestions on our work. The following is our response to the reviewer’s comments and questions.\n\n### **1. Absence of Deepseek-Prover-V2 from Related Works**\nDeepseek-Prover-V2 got released on the edge of the submission deadline and we could not properly test the model with Apollo. To remedy this, we performed experiments on the current state-of-the-art medium-sized prover: Goedel-V2-8B [1]. Our experiments show that Goedel-V2+Apollo solves four more problems in miniF2F-test, which constitutes a _1.6% gain in accuracy_. \n\nWe will add the discussion of newer whole-proof generation models in the revised manuscript.\n\n### **2.  Comparing true sampled budgets of Apollo and base provers**\nWe agree with the reviewer that comparing an upper bound to the fixed passK parameter is not entirely fair. To remedy this, we consider two settings: observed upper bound and average number of sampled proofs across the entirety of miniF2F-test, including the failed proofs. For Apollo, we consider only theorems that were not proved by the base LLM, and for the base LLM we consider all attempted problems. The results are below:\n\nTable 1: Average and upper bound sampling budgets for base LLMs and Apollo aided proofs\n| model               | upper bound | average budget | accuracy |\n|---------------------|-------------|----------------|----------|\n| goedel-sft          |       25600 |           9730 |    64.7% |\n| kimina-7b           |        1024 |            373 |    70.8% |\n| goedel-sft + Apollo |        1100 |            618 |    65.6% |\n| kimina-7b + Apollo  |         888 |            367 |    75.0% |\n\n\nWe observe that the average number of sampled proofs increases for Apollo when failure cases are included. For Goedel-SFT, gains remain substantial, as the base LLM attempts each problem many times up to 25,600. For Kimina-Prover, the average budgets with and without Apollo are similar, yet Apollo achieves higher accuracy with a lower maximum number of sampled proofs. Additionally, miniF2F contains a sizable number of easy problems that LLMs typically solve within 1–8 attempts, skewing base-LLM results toward lower counts. We omit these easier theorems from the Apollo evaluation, since Apollo did not participate in their proofs. Even under these conditions, Apollo matches or reduces sample complexity compared to the base LLMs while delivering accuracy improvements across the board.\n\n### **3. Comparing Apollo to MCTS-based sampler**\nWe would like to clarify that the Apollo framework differs from traditional tree-search methods. Our approach decomposes a theorem into independent sub-proofs, identifies the failing ones, and proves them recursively. Because each sub-goal is independent, these repairs can be performed in parallel. Unlike tree search, Apollo does not conduct an explicit search during inference; instead, it iteratively patches the initial proof attempt until it reaches a correct solution.\n\nTo compare Apollo with a different MCTS-based sampling strategy, we have run Kimina-Prover-Distill-7B with the RMaxTS search method proposed by [2]. The results are below:\n\nTable 2: Comparing Apollo to RMaxTS sampling strategy\n\n| method        | budget (max sample count) | budget (tokens) | accuracy |\n|---------------|---------------------------|-----------------|----------|\n| kimina-7b        |             32            |       140K      |   63.1%  |\n| kimina-7b        |            1024           |       4.5M      |   70.8%  |\n| kimina-7b+RMaxTS |          4 x 128          |       2.0M      |   64.3%  |\n| kimina-7b+Apollo |            589            |       2.2M      |   75.0%  |\n\nWith similar token budgets, Apollo significantly outperforms RMaxTS strategy and vanilla whole proof generation method. Although Apollo’s worst-case budget slightly exceeds RMaxTS, its average budget is lower. Apollo generated 307 proofs and 1.3M tokens on average, which is substantially lower than the RMaxTS strategy.\n\n### **4. Accuracy scale with large recursion depth $r$**\nWe decided to stop sampling once the performance curve plateaued and examined the outputs. Because Apollo’s effectiveness relies heavily on the underlying base model, it diminishes when the LLM has little idea on how to proceed. Our analysis shows that many failures arise from models re-proving given steps or hallucinating. Increasing recursion depth yielded no accuracy gains. We believe this plateau reflects the prover’s inherent quality, its problem-solving ability and capacity to generate high-quality proof sketches. At the time of this work, proof sketching existed only in external tools like DSP [3], not within provers themselves. We expect this to change soon, as new theorem provers begin to include high-level proof sketches and informal reasoning in their chain-of-thought outputs.\n\n### **5. Subset of reported proofs in Figure 4**\nYes, the figure only visualizes the proof length of valid proofs. We will make this point clear in the revised manuscript.\n\n### **6. Relationship between $r$, sample budget and token count**\nBelow are tables of the relationship between sample budget, recursion depth and token count for two theorem provers: Kimina-Prover-Preview-Distill-7B and Goedel.\n\nTable 3: Relationship between $r$, sampling budget and token count on Kimina-Prover-Preview-Distill-7B.\n| rec depth     |    0 |    2 |    4 |    6 |\n|---------------|-----:|-----:|-----:|-----:|\n| sample budget |   32 |   96 |  191 |  307 |\n| token count   | 140K | 406K | 816K | 1.3M |\n\n\nTable 4: Relationship between $r$, sampling budget and token count on Goedel-SFT.\n| rec depth     |     0 |     2 |     4 |    6 |\n|---------------|------:|------:|------:|-----:|\n| sample budget |    32 |    80 |   151 |  362 |\n| token count   | 16.1K | 38.3K | 74.6K | 179K |\n\nWe observe that the sample budget and token count depend linearly on the recursion depth $r$. We will convert these tables into plots and include them in the revised manuscript.\n\n### **7. Applying @N on top of Apollo**\nYes, it is possible to apply @N at each iteration of the framework. Increasing @N results in more sampled proofs per sub-goal, giving the LLM additional opportunities to generate a valid proof. Conversely, increasing $r$ leads to deeper sub-goal decomposition and greater simplification of each sub-goal. A higher $r$ parameter allows Apollo to explore each sub-goal more thoroughly and increases the likelihood that it will be further decomposed. \n\nThroughout our experiments with @N fixed at each recursion iteration, we consistently improved the baseline accuracies of all theorem provers while reducing computational costs. Goedel-SFT’s accuracy increased by 0.9%, and its sampling budget decreased from 25,600 to 362. Kimina-Prover-Preview-Distill-7B saw a 4.2% improvement while using only one-third of the sampling budget. General-purpose models jumped from a few percent to over 40% accuracy. Our experiment also shows that the performance of even the latest theorem provers, such as Goedel-V2, can be further enhanced. Increasing the @N parameter could yield additional gains and serve as an extra hyperparameter in the Apollo framework.\n\n---\n\nThank you again for your thorough feedback. Your comments have helped clarify our paper, and the revised version will offer deeper insights into agentic Apollo repair. In light of these improvements, we hope you might consider increasing your score. If you have any further questions, please don’t hesitate to let us know.\n\n---\n\n[1] Yong Lin, et al. (2025). Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date.\n\n[2] Huajian Xin, et al. (2025). DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. In The Thirteenth International Conference on Learning Representations.\n\n[3] Albert Qiaochu Jiang, et al. (2023). Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations."}]

Author rebuttal:

Meta-review: I recommend accepting this paper. APOLLO combines Lean compiler feedback with LLM reasoning to improve automated theorem proving, achieving 75% accuracy on miniF2F while reducing sampling costs, and boosting general-purpose models from 3-7% to over 40% accuracy. Reviewers (scores: 3, 4, 5) recognized its valuable contribution in integrating compiler feedback effectively across different models, demonstrating how targeted repair can significantly improve formal reasoning efficiency.
Decision: Accept (poster)