APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

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.

1. Absence of Deepseek-Prover-V2 from Related Works

Deepseek-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.

We will add the discussion of newer whole-proof generation models in the revised manuscript.

2. Comparing true sampled budgets of Apollo and base provers

We 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:

Table 1: Average and upper bound sampling budgets for base LLMs and Apollo aided proofs

We 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.

3. Comparing Apollo to MCTS-based sampler

We 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.

To 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:

Table 2: Comparing Apollo to RMaxTS sampling strategy

With 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.

4. Accuracy scale with large recursion depth $r$

We 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.

5. Subset of reported proofs in Figure 4

Yes, the figure only visualizes the proof length of valid proofs. We will make this point clear in the revised manuscript.

6. Relationship between $r$, sample budget and token count

Below are tables of the relationship between sample budget, recursion depth and token count for two theorem provers: Kimina-Prover-Preview-Distill-7B and Goedel.

Table 3: Relationship between $r$, sampling budget and token count on Kimina-Prover-Preview-Distill-7B.

Table 4: Relationship between $r$, sampling budget and token count on Goedel-SFT.

We 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.

7. Applying @N on top of Apollo

Yes, 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.

Throughout 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.

---

Thank 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.

---

[1] Yong Lin, et al. (2025). Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date.

[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.

[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.

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.

1. Apollo against iterative feedback repair

Indeed, 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:

Table 1: Comparing feedback repair to Apollo repair with o3-mini as the base model

Feedback prompt schema:

This is an incorrect proof:
[model’s last proof]
Compilation errors are as follows:
[Lean’s error messages]
Based on this feedback, produce a correct raw Lean code for the following problem:
[header]
[informal prefix]
[formal statement]

To 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.

2. CPU and GPU bottlenecks in theorem proving

Indeed, 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.

By 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.

We 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.

We will include this discussion in the revised manuscript.

3. Additional information on connection between sampling costs and recursive calls

To 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.

Table 1: Relationship between $r$, sampling budget and token count on Kimina-Prover-Preview-Distill-7B.

Table 2: Relationship between $r$, sampling budget and token count on Goedel-SFT.

4. Ablation studies

We 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.

Table 3: Ablation study of different parts of Apollo on o4-mini (general purpose model) and Kimina-Prover-Preview-Distill-7B (theorem prover model)

For 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.

By 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.

To further investigate each module, we conducted a simple test to see how many times each module was called during an inference.

Table 4: Number of Apollo module triggers across different models

Across 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.

We 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.

5. Relevance of recursive repair

We 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.

Moreover, 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.

To 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.

---

Thank 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.

---

[1] Haiming Wang, et al. (2025). Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models.

[2] Yong Lin, et al. (2025). Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date.

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.

1. Reporting token budget vs accuracy across the board.

Comparisons lack consistency in model and token budget; more datasets are needed.

As 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.

Table 1: Performance of base Kimina-7B against LLM with Apollo on ProofNet dataset

Table 2: Performance of base Kimina-7B against LLM with Apollo on PutnamBench dataset

We observe that applying Apollo improves the accuracy across both benchmarks while reducing the number of generated tokens compared to the base LLM.

2. Limited generalizability

Modules rely on hand-crafted rules, limiting generalizability.

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.

It 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.

Apollo 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.

To 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.

3. Comparing Apollo to alternative sampling strategies.

No comparison with standard depth-first or best-first search methods.

Per 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.

Table 3: Comparing Apollo to RMaxTS sampling strategy

Per 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.

4. Contribution of agentic Apollo framework

Clarifying how Apollo differs from standard modular repair workflows or existing agentic frameworks would help assess its conceptual contribution.

Although 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.

Agentic 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.

5. Using tree search strategies for token budget reduction

We 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.

6. Additional reproducibility components

We 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.

---

We 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?

---

[1] Taicheng Guo, et al. (2024). Large Language Model Based Multi-agents: A Survey of Progress and Challenges. IJCAI.

[2] Junde Wu, et al. (2025). Agentic Reasoning: A Streamlined Framework for Enhancing LLM Reasoning with Agentic Tools.

[3] Chen Qian, et al. (2025). Scaling Large Language Model-based Multi-Agent Collaboration. ICLR