MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
Authors: Ruida WANG
Rui Pan
Yuxin Li
Jipeng Zhang
Yizhen Jia
Shizhe Diao
Renjie Pi
Junjie Hu
Tong Zhang
Venue: ICML 2025 poster (2025)
Keywords: LLM reasoning
math QA
Lean4
Primary area: deep_learning->large_language_models
TL;DR: This research presents the MA-LoT framework, a novel framework that enhances the Lean4 reasoning ability of LLMs by allowing collaboration between prover and Lean executors using Long CoT with formal reasoning ability.

Abstract: Solving mathematical problems using computer-verifiable languages like Lean has significantly impacted the mathematical and computer science communities. State-of-the-art methods utilize a single Large Language Model (LLM) to generate complete proof or perform tree search, but they fail to balance these tasks. We propose **MA-LoT**: *Model-CollAboration Lean-based Long Chain-of-Thought*, a comprehensive framework for Lean4 theorem proving to solve this issue. It separates the cognition tasks of general NL for whole-proof generation and error analysis for proof correction using the model-collaboration method. We achieve this by structured interaction of the LLM and Lean4 verifier in Long CoT. To implement the framework, we propose the novel *LoT-Transfer Learning* training-inference pipeline, which enables the Long CoT thinking capability to LLMs without special data annotation. Extensive experiment shows that our framework achieves a **61.07%** accuracy rate on the Lean4 version of the MiniF2F-Test dataset, largely outperforming DeepSeek-V3 (33.61%), single-model tree search (InternLM-Step-Prover, 50.70%), and whole-proof generation (Godel-Prover, 55.33%) baselines. Furthermore, our findings highlight the potential of combining Long CoT with formal verification for a more insightful generation in a broader perspective.

MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
Ruida Wang" Rui Pan
Yuxin Li Jipeng Zhang² Yizhen Jia
Shizhe Diao
Renjie Pi Junjie Hu" Tong Zhang'
Abstract
1. Introduction
Formal reasoning is cornerstone of human intelligence and a key objective in machine learning (Newell & Simon, 1956). often evaluated through rigorous mathematical deriva- tions (Yang et al., 2024a). With the rise of Large Language Models (LLMs), Chain-of-Thougee (CoT) prompting has emerged to formalize reasoning by generating intermediate steps. This approach improves interpretability and enhances reasoning performance (Wei al., 2022).
Solving mathematical problems using computer- verifiable languages like Lean has significantly impacted the mathematical and computer sci- ence communities. State-of-the- art methods uti- lize single Large Language Model (LLM) to generate complete proof or perform tree search, but they fail to balance these tasks. We pro- pose MA-LoT: Collbbr-Clll Lean-based Long Chain-of Though,, a comprehensive frame- work for Lean4 theorem proving solve this is- suc. It separates the cognition tasks of general NL for whole-proof generation and error analysis for proof correction using the model-collaboratin method. We achieve this by structured interac- tion of the LLM and Lean4 verifier in Long CoT. To implement the framework, we propose the novel LoT-Transfer Learning trining-inferenee pipeline, which enables the Long CoT thinking ca- pability to LLMs without special data annotation. Extensive experiment shows that our framework achieves a 61.07% % accuracy rate on the Lean4 ver- sion the MiniF2F-Tes dataset, largely outper- forming DeepSeek-Ve V3 (33.61 %), single-model tree search (IntemLLM-Step-Provee)) 50.70%), and whole-prood generation (Godel-Prover, 55.33%) baselines. Furthermore, potential of combining Long CoT with formal verification for a more insightful generation in broader perspective.
tatral eor
Rein
Theorem
Woona atule
Andee peneration
Amalysis
Complene
peoof
Prro
Tree-Search Method:
Whole-proof generation
Use ITP to chock
LLM NL planning and reasoming
Find non-trivial proof
Controllable
Expensive
No intermediate feedhack
No Long-ternn NL. planning
Usually trivial solution
Figure I. Two main directions of FL theorem proving using LLMs: Single model tree-search and whole-proof generation with their advantages/disadvanntees
However, the ambiguity of Natural Language (NL) compli- cates verifying intermediate steps, particularly in advanced mathematics, where there is answer check but theo- rems to prove. This challenge is exacerbated by the growing complexity of modern mathematics, which makes proof ver- ification highly demanding and can lead to eπrоrs, seen in the prolonged validation of Fermat's Last Theorem (Wang et al., 2024). Researchers propose grounding reasoning in rigorous first-order logic to address this, enabling automated verification via Formal Language (FL) verifiers. This frame- work ensures rigor and has led the development of tools like Lean (De Moura et al., 2015; Moura & Ullrich, 2021). Isabelle (Paulson, 1994), and HOL Light (Harrison, 2009) for verifiable theorem proving.
findings highlight the
First Authors 'Department of Computer Science, University of Illinois Oobann-Chammaainn 'Hong Kong University of Science and Technology 'NVIDIA 'Department of Computer Science, University of Wisconsin- Wisconsin-Madison. Correspondence to: Ruida Wang <ruidaw idu...
Proceedings of the ndnd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
However, writing mathematical proofs in FL requires signif- icant expertise and effort, as most proofs involve extensive

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of- Chain-of-Thought Reasoning enhances Formal Theorem Proving
Prompt
Prompt
LoT-Solver Prover
LoT-Solver Corrector
Lo---eleer
1s Proof
2d Proof - Rethink prompt
as Corrector
Rethink prompl
NL-Planning CoT
Error analysis
Error analysis CoT-2
Prompt
CoT-1
1 Proof
2nd Proof
3 Proof
Proof Done
Proof Done
(a) Model-Collaboratinn Lean-based Long CoT inference
Training data sample
fererncce data sample
Saatem Premut:: Comples the following Leand mooren WITHIOT Long Coi
System Pronee: Complete the the following Leart incorom WITH Long Col
by
eve
Show it tale ther Proof coctndiction
Show that ia false A.s... Phoof conmadiction
Inferenced part
Lean SFT
FL
Asd EL statenent:
thcorem and adf: -f-AAA)
<Thoughe>
<Thorght>
step-hy-
Thoudh
Commented Theeesm:
Compleied proof
Complaed and
Beveaa and sell a
Prouf by contrstiaioon [Ehr, hoj so hn
by contidiction
contmatatioon
Trained part
(b) LoT-TL Training-Infee Inference pipeline
Pretrained LLM
General NI. I Long
Lean SFT data (LoT::11.
Lean Correction data (LoTI:IL)
LoT-Solver
CoT data (SFT)
(c) Training procedure of LoT-Solver
Figure MA-LoT Framework: (a) Model-collaboration Lean4 theorem proving framework: The LoT-Solver model functions as the prover to generate initial Lean4 proofs with emergent NL planning for Lean proof in Long CoT (orange block); then acts corrector to analyze error from Lean executor in Long
to output refined proof. (b) LoT-Transfer Learning (TL): novel training-inference pipeline enables formal reasoning ability emerge in Long CoT (L-CoT) without the need for specifically annotated data. This is achieved by adjusting the system prompt to control the on/off L-CoT in training and inference. (c) Training procedure LoT- We normal SFT train general NL L-CoT, LoT-TL to train the Lean SFT, and correction data make Lean L-CoT emergent capability in LLM.
repetition and application of low-resource functions (Jiang et al., 2022). With the rapid progress of LLMs, research has explored L.MSs application in FL reasoning to auto- mate theorem proving (Polu & Sutskever, 2020; Polu et al., 2022; Jiang et al., 2021; 2022; Yang et al., 2024b; Xin et al., 2024b; Wang et al., 2024; Wu et al., 2024a; Kumarappan al., 2024; Lin et al., 2024). Prior research follows two main approaches, namely, tree-search (Jiang al., 2021; 2022; Lin et al., 2024; Xin al., 2024b; Wang et al., 2024) and whole-proof generation (Polu& & Sutskever, 2020; Polu et al., 2022; Yang et al., 2024b; Wu et al., 2024a; Kumarap- pan et al., 2024). The summary of dis/advantages of these two methods can be found in Figure 1.
writing (Polu & Sutskever, 2020; Polu al., 2022; Xin et al., 2024b; Wu et al., 2024a; Lin et al., 2024) retrieval- based techniques (Yang et al., 2024b; Kumarappan et al., 2024). Tree-search methods apply an FL executor to verify after each generation step and can discover some non-trivial proofs. However, as proof complexity increases, tree-search methods become computationally expensive and lack high- level NL planning control the overall structure of the proof. The lack of overall planning causes the tree-search method to be unable to find some structured proof that requires high-level NL planning to answer the question.
In contrast, whole proof generation treats theorem proving like the code generation problem, where LLMs generate the entire proof in single attempt using either supervised training (Wang et al., 2024; Xin et al., 2024b) or prompt en- gineering (Jiang et al., 2021; 2022). This approach leverages
Tree-search methods train an LLM iteratively generate proof steps by predicting the next tactic based on the current proof state. This is achieved through either direct code
2

---

MA-LoT: Model-Collaboration Lean-based Long Shain-of-Thoughh Reasoning enhances Formal Theorem Proving
LLMs' NL reasoning and high-level planning capabilities with predictable computation costs, but it lacks intermediate feedback from FL executors. As a result, the generated proofs often lack post-hoc analysis of errors and tend to perform badly on tedious questions that require non-trivial or tedious tricks. In summary, existing single-model ap- proaches struggle to balance the NL reasoning with the FL verifiability, motivating the need for a more comprehensive framework.
ing state-of-the-art whole-proof generation models (Godel- Prover (Lin et al., 2025), 55.33%) and tree-search baseline (IneemLM-ssee--ProveeWW et al., 2024a), 50.70%).
We summarize our contributions as follows: (1) We in- troduce MA-LoT, a comprehensive model-collaboration framework to balance NL reasoning and FL verification under the Long CoT paradigm for Lean4 theorem proving, (2) We propose using Long CoT to synergically combine the nature of NL and FL. allowing the model to generate in- depth and insightful formal reasoning through NL planning and analysis. (3) We develop LoT-TL, training-inferenc pipeline that makes field-specific Long CoT capabilities emerge to LLMs without requiring explicitly annotated datasets.
To address the above challenges in Lean4 theorem proving, we introduce MA-LoT: Grodel-CollAboration tean-based Long Ohaii--ofThhuuhhe a comprehensive framework de- signed to coordinate multiple models for effective formal reasoning. As illustrated in Figure (a), MA-LoT sepa- rates the cognitive process into two distinct tasks: high-level proof planning and writing, well fine- grained correc- tion based on verifier feedback. This separation is enabled by a collaborative model architecture and the emergent rea- soning capability of Long CoT, which was developed during training. The framework consists of two core components: a prover model, responsible for generating well-structured proofs, and a corrector model, which interprets feedback from the Lean4 verifier refine the output. Both models enhanced with Lean4 field-specific Long CoT capability, allowing them to reason more thoroughly before producing outputs. Moreover, we integrate Lean verification results into Long CoT to improve the system's 's self-reflcttion and correction abilities.
Our framework has broad potential beyond Lean4 theorem proving, demonstrating how formal verification can be effectively integrated with Long CoT reasoning. This approach reveals the potential for structured, reflective, and adaptable general text generation through iterative planning and error analysis on formal executors. To accelerate advancements in this field, we open-source our code at http://hhhhh..oommkckk///wwv/eet Official
2. Methodology
In this section, we detail the development of the MA-LoT framework and training procedure of LoT-Solver model for Lean4 theorem proving. Our framework's 's core idea is to enable the model perform Long Chain-of-Thought (CoT) reasoning under the context of Lean4 theorem proving, The Long CoT is designed to perform deep integration between Natural Language (NL) and Formal Language (FL) reason- ing. Training of such Long CoT thinking model is achieved under an extreme scarcity of NL-FL aligned data faced by the entire field (Wang et al., 2024). We introduce the methods by first outlining the preliminaries of LLM for- mal theorem proving in Section 2.1. Then, describe the LoT--ransser Learning (LoT-TI.) training pipeline in Section 2.2. Finally, we present comprehensive details on how our trained model facilitates MA-LoT framework for Lean4 proof writing in Section 2.3.
To implement the MA-LoT framework, we propose a novel training-inference pipeline called LoT-Transfer Learning (LoT-TL), which is used to train the LoT-Solver model, as shown in Figure 2 (b) and (c). This pipeline enables the emergence of using Long CoT to solve the FL. problems without requiring specifically annotated formal data. It is achieved by leveraging transfer learning across three data sources: NL-based general Long CoT reasoning, SFT data for theorem proving under the code completion task, and in/correct proof pairs based on Lean4 feedback. Through structured adaptation, LoT-TL. equips the model with aware- ness of FL proof states and tactics while preserving its strong NL reasoning and planning capabilities. Then, the model trained under this pipeline can generate coherent and in- sightful formal proofs grounded in both symbolic precision and hivel planning.
2.1. Preliminaries
Extensive experiments demonstrate that MA-LoT frame- work effectively enhances the model's formal reasoning ability through model-collaboration design and emergent formal reasoning in Long COT. The framework can success- fully prove some of the advanced IMO and AIME problems in the MiniF2F dataset (Zheng et al., 2021), with which existing models struggle. Under similar sampling budgets, our framework achieves a 61.07% accuracy rate, surpass-
We introduce preliminary knowledge of applying Long Chain-of- (CoT) LLMs to Lean4 formal theorem proving in a model-coollaboration manner.
Current sfate-of-the-ard methods treat Lean4 code as plain text and feed it directly to LLMs. There two main branches of techniques to apply LLMS for Lean4 theorem proving. The first branch is the tree-search method (Yang et al., 2024b; Wu et al., 2024a). This method converts the
3

---

MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thone Thought Reasoning enhances Formal Theorem Proving
Lean4 theorem statement and current proof state (includ- ing conditions and goals based the existing proofs) into plain text as input to LLMs and asks it to generate the next possible tactic to complete the proof. The other direction is whole-proof generation methods. It provides the I.LMs with NL instruction, NL theorem statement, and Lean4 state- ment to the LLMs. The intended outcome is to generate complete Lean4 proof in a single pass. This is achieved by first leveraging the LLM's NL reasoning to produce high-level plan, then guiding the generation of the actual Lean4 proof The input-output examples for both tree-search and whole-proof generation are presented in Appendix B.
OBT (Wang al., 2024)), lack Lean4 proofs (e.g., Lean- Workbook (Ying al., 2024)).
To address this, we compile a new Lean theorem proof dataset named LoT-ProveData (LoT-PD), containing 54,465 data records. Each record contains Lean4 theorem state- ments, verified proofs with NL explanations as comments, and NL statements. The Lean4 theorem proofs come from two sources: the DeepSeck-Proverss dataset and the annotated Lean- Saan-Wrrbbook using TheoremL and Prooeek---rve---l..
Next, inspired by the analysis- then generate approach in Wang et al. (2023), we employ Qwen-2.5-7225 to provide an analysis of Lean4 proofs, fol- lowed by writing the NL proof based on the analysis. Fi- nally, we integrate these NI. proofs as comments in the Lean4 code by Qwen. For data records lacking NL state- ments, we generate NL statements using similar method. The core components of our LoT-ProveData are as follows:
The Long CoT LLMs, represented by O1 (OpenAI, 2024), make long internal NI. thinking before outputting the final answer. It largely enhances the NL math reasoning ability of LLMs through self-reflection and correction in Long CoT. However, it still struggles to provide rigorous NL proofs and typically has relatively low FL capability.
(FL Statement, Commented FL proof, NL statement.)
Our approach combines the strengths of tree search and whole-proof generation methods through a model- collaboration system. By leveraging Long CoT, we coordi- nate the interaction between NL and FL in LLMs, which allows the model to write more structured and insightful proofs.
During proof generation for the ProverData, some incor- rect proofs were also produced. We recorded these along- side their error messages to form LoT--CorecciinDaat (LoT- CD), consisting of 64,912 records of correct-incorrect Lean4 proof pairs with error messages of the incorrect proof. Ad- ditionally, it contains an NL statement and proof of the theorem. LoT-CD is used to train the model'ss 's error analysis and correction capability. The core part of the LoT-CDD is:
2.2. LoT-TL Training Pipeline
This section introduces simple but effective training pipeline LoT-Transfer Learning (LoT-TI... The pipeline in- tends to make LLMs have the ability to perform Lean4 field-specific Long CoT reasoning. Such ability can be ob- tained through LoT-TL without the need for specifically annotated Long CoT data. The main idea of LoT-TL is to leverage system prompts to regulate training and infer- ence behaviors, which can be divided into the following stages: (1) collecting field-specific Supervised Fine- mineiTunigg (SFT) data (Section 2.2.1), (2) training the model on general natural language Long CoT tasks (Section 2.2.2), and (3) training the model using the transfer learning method on SFT and correction data to make formal Long CoT abil- ity emerge(Section 2.2.3). Although this paper focuses on Lean4, our framework shows potential to be applied to more fields, making LLMs obtain field-specific Long CoT capa- bility without RL or special data annotation.
{ [FL Statement, Correct FL proof, Error messages, Incorrect FL proof, NL statement)
These datasets work together to improve both the prover and corrector models' capability, acting as the source of strong NL-FL joint thinking ability for our model-collaboration framework.
2.2.2. NL LONG COT TRAINING
In the second stage, we train normal instruction cestruction-finetueed model to obtain the general Long CoT reasoning capa- bility in Natural Language. We use the OpenO1-SFT- Pro dataset provided by Open-Source-01 (2024), a 126k records dataset for general NL pnuestion-answeriig on math and science topics with Long CoT for training. We apply standard next-token prediction SFT, guiding the model to produce Long CoT before it outputs final answers. Through- out the NL Long CoT training, we set the system prompt as follows to explicitly instruct the model to use the Long CoT approach:
1.2.1. OBTAIN SFT DATA
The first step of LoT-TL pipeline is to gather a moderate amount of NL. aligned SFT data for the specific target field (in our case, Lean4). However, existing open-source datasets do not meet the requirement. They are typically small in size (e.g., MiniF2F (Zheng et al., 2021)), or omit NL annotations (e.g., Peeveeee-Proverrvv dataset (Xin et al., 2024a)), or exhibit relatively low NL quality (e.g..
You are helpful assistant who will solve every problem **WIT*** Long Chain-of-Thought

---

MA-LoT: Model-Collaboration Lean-based Long Chain-of- Thought Reasoning enhances Formal Theorem Proving
This system prompt indicates that the model should use the Long CoT to write the answer. The training input includes the system prompt and NL question, with the expected out- put being the Long CoT and final answer. After training, we observe that the model gains robust NL Long CoT ca- pabilities, which serve as a base for models to analyze and interact with Lean code. However, when applied to Lean4 reasoning, tends to provide only NL solutions rather than outputting Lean4 code in its output section, indicating the need for further alignment.
and tree-search methods under the Lean-based Long CoT paradigm. We use the Lo'--Solver as the base model for both the prover and the corrector. Under this setup, use the prover model to write a complete proof draft (Section 2.3.1) 1) and apply the corrector model to analyze and correct the proof based on Lean verifier feedback (Section 2.3.2).
2.3.1. PROVER MODEL
The prover model writes the initial Lean4 proof using a whole-proof generation strategy. Then, it is submitted to the Lean4 verifier to check its correctness and passed to the corrector model if it is wrong. We use the system prompt to turn on the Long COT reasoning and use a specific header in Long CoT to guide the model in making a high-level proof plan. Here is the instruction template for the prover model:
2.2.3. FIELD-SPECIFIC ALIGNMENT
In the final stage of the training process of LoT-TL pipeline, we train the model to obtain emergent Lean4 Long CoT ability. In this training stage, we set the system prompt to instruct the model not to use Long CoT when answering. In the meantime, to make the model aware of the Long CoT structure, we use a simple placeholder to occupy the original place of the Long COT. The above method allows us to train the model aware of the Lean4 Long CoT structure without requiring any Lean4 Long CoT data. Specifically, the system prompt is:
(... **ITH*** Long CoT ...)
#*# Instruction:
(NL statement]
(FL statement)
#*# Response:
Airight, I should do the following:
1. Provide the natural language analysis for the theorem based on the Natural language theorem
You are a helpful assistant who will solve every problem **WITHOUT* Long chain-of-Thought
statement.
2. Draft the Lean4 tactics I should use
and the placeholder Long CoT is:
4 to solve the problem
3. Write the output Lean4 code.
The user asks not to solve with Long + CoT, so will directly write the answer.
The prover model's input and output example can be found in Appendix G. The emergent Lean reasoning ability the Long CoT enables the model to write a better-structured proof based its high-level plan than direct proof genera- tion. Upon generating the proof, the prover model submits it to the Lean evaluator for verification. The theorem is then passed to the corrector model for further refinement if incorrect.
Under this setup, we first train on the LoT-ProveDaata for formal theorem proving ability, then train on the LoT- CorrectionData make the model learn analsss and correction skills. The example of training data can be found in Appendix F. We also adopt the curriculum learning data sorting method from Wang et al. (2024) to stabilize training. After training, we find that the Long CoT Lean4 proving and error analysis ability emerges in the LLMS when using the system prompt to turn on Long CoT in inference. We conclude the effectiveness of the TI. framework because it preserves the structure of Long CoT and enables the model to activate such capability when instructed.
2.3.2. CORRECTOR MODEL
After receiving wrong proof and Lean verifier feedback, the corrector model will systematically analyze them in Long COT. The corrector re-evaluates and rethinks the proof strategy, then generates a revised proof that intends to cor- rect the errors and complete the proof. In conceptual anal- ogy, the corrector model functions similarly to the tree- search method but with greater flexibility and deeper analy- sis.
Following the above steps, we train the LoT-Solver model based on an expert Lean4 prover with instruction fine-tuning. LoT-Solver is a model with Lean4 Long CoT reasoning capability, which also enables the separation whole-proof writer and corrector.
The instruction prompt remains identical to the prover model. We incorporate the incorrect proof and feedback from the Lean verifier in the Long CoT, followed by instruc- tions to direct the model to analyze the error and formulate a revised proof. Detailed examples of such prompts are available in Appendix G. Then, the corrector model will
2.3. Coleb--ollabooration Lean4 Proof Writing
This section presents the model-colllaboration framework that combines the advantages of whole-proof generation
5

---

MA-LoT: Model-Collaboration Lean-based Long Chain-of-Tharn Thought Reasoning enhances Formal Theorem Proving
pass the new proof the Lean4 verifier. If the new proof is still wrong, iteratively analyze the errors until success or reach the max retry limit.
3.1.2. BASELINES
To highlight MA-LoT 's capabilities, we select some of the most competitive baselines in recent years, cov- ering both tree-search and whole-proof generation ap- proaches. For tree-search methods, we include: Expert Iteration (Polu et al., 2022), Llemma (Azerbayev et al., 2023), ReProver (Yang et al., 2024b), Lean-STale STaR(LiTTRRnn et al., 2024), and IncemL.2..-StepProoerr (Wu et al., 2024a) as our baselines. For whole-proof generation baselines, we include closed-source L.MSs, represented by GPT-4-Turbo( Acchamm et al., 2023), Ceminii-.5(RRea et al., 2024), and DeepSeek- V3 (Liu et al., 2024). Moreover, we include representative open-sourge expert models for whole- chole- writing, such as SeepSeee-Matt(Shane et al., 2024), aaboremmJaaaa Wang et al., 2024), PerpSeeck-rove--I.555 STa-Lean (Dong & Ma, 2025), and Godel-Prover-SS Prover-SFT (Lin et al., 2025).
The corrector model enhances theorem proving by enabling deeper reflection and systematically exploring alternative proof strategies based on error messages. This iterative cor- rection process increases the likelihood of discovering non- trivial proof' while maintaining computational efficiency.
3. Experiments
We conduct comprehensive experiments on the MiniF2F- Lean4 (Zheng et al., 2021) dataset to assess the perfor- mance of the MA-L.OT framework in formal proof writ- ing. Specificallyy, we intend to prove the advantage of the MA-LoT framework by showing its capability to generate better-structured and more insightful proofs. We do this by showing our model has a better general performance in Section 3.3. Moreover, we perform studies on our correc- tor model in Section 3.4, the efficiency of the Long CoT method in Section 3.5, training components of LoT-Solver in Section 3.6, and case study in Section 3.7 to further analyze the impact of individual components.
(Xin et al., 2024b)²,
For whole-proof generation baselines, we set the sample budget to pass@ 128 with 4096 context length (except for Godel-Prover, where, following the original paper, we use pass @ 32), balancing robustness and manageable GPU con- sumption. We align the search cost as closely as possible for tree-search methods to whole-proof generation."
3.1. Experiment Setup
3.2. Implementation Details
3. DATASET AND TASK
In the model's training process, we use Openol-SFT-Pree LoT-ProverData, and LoT-CorrettionDaata to train two base models, namely LaapSeee--Proee-vlll
In this paper, we assess MA-LoT's Lean4 reasoming capabil- ities on the MiniF2F-Test and Valid' datasets (Zheng et al., 2021; Yang al., 2024b; Wang et al., 2024). MiniF2F is widely used and challenging benchmark for formal theorem proving (Frieder et al., 2024), which is adopted in nearly all major studies in the field (Jiang et al., 2021; Polu et al., 2022; Jiang et al., 2022; Wu et al., 2024a; Lin et al., 2024; Yang et al., 2024b; Xin et al., 2024b; Wang et al., 2024; Azerbayev et al., 2023).
and Godel- PFover-SFT. For different training stages, the learning rate is as follows: 1E-5 for NL Long CoT training, 1E-7 for LoT- TL on LoT-PD, and 1E-6 for LoT-CD. The total computa- tional cost for training is around GPU day, and evaluation is 11 GPU days on a 4x H100-96G cluster'. To evaluate our framework in detail, we present three sets of results, including: (1) LoT (whole-proof): pass @ 128 whole-proof generation result of LoT-Solver. (2) MA-LoT: Our primary evaluation result, where the prover performs 64 whole-proof generations and undergoes two rounds of corrector refine- ment'. (3) Cumulative Results: A combined evaluation aggregating all LoT models' outputs obtained throughout
Both the test and validation datasets contain 244 Lean4 state- ments. The range of problems varies from high-school com- petition questions to undergraduatt-level theorem proofs. It includes 488 problems from three sources: (1) 260 problems sampled from the MATH dataset (Hendrycks et al., 2021); (2) 160 problems from high school math competitions, in- cluding AMC, AIME, and AMO; (3) 68 manually crafted problems at the same difficulty level as (2). Our task is to query the LLM to generate Lean4 proof's for MiniF2F prob- lems based on their formal statements and NL descriptions. To minimize computational overhead, imports are manually configured.
high-school
"The reported results of DeepSeek- DeepSeck-Prover-V 1.5 and Goedel- Prover in our paper are different from the original paper because unable to access vLLM in our machine, and it is known that the inference without vllm will lead to slight drop of the model's s capability
"This explains why we exclude RMaxTS for DeepScek-Prover. v1.5, as its smallest disclosed sample budget (1 3200) is not a comparable result to our baselines.
"The high evaluation cost is duc accelerated inference meth- ods like vLLM being unable to fit our machine
Although DeepScck-Proverts .5 declared that they applied MiniF2F-Vall for training, yet its performance does significantly differentiate from other methods. Thus, we still keep this baseline.
'Because we don't 'on't need to pass a correct proof to the corrector, two rounds of correction approximately the same as one round of whole-proof generation
6

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thougee Reasoning enhances Formal Theorem Proving
Method
Model size
Sample budget
MiniF2F-Vaill
MiniF2F-Test
Average
Tree-search Methods
ReProver (Yang et al., 2024h)
229M
26.5%
Llemma (Azerbayev et al., 2023)
34B
x 32 x 100
27.9%
25.8%
26.85%
Expert Iteration (Polu et al., 2022)
837M
8 x 8 x 512
41.2%
36.6%
38.9%
Lean-STaR (Lin et al., 2024)
7B
64 x 1 50
46.3%
Se.ern.M2.5-StePPrron (Wu et al., 2024a)
7B
x 32 x 600
56.0%
50.7%
53.35%
Whole-proof generation
GPT-4-Turbo (Achiam et al., 2023)
1T
25.41%
22.95%
24. 18%
DeepSeek-Math (Shao et al., 2024)
25.80%
24.60%
25.20%
Gemini-1.S-pro (Reid et al., 2024)
29.92%
27.87%
28.90%
pass @ 128
TheoremL.amaa (Wang et al., 2024)
38.52%
35.66%
37.66%
DeepSeek-Prooerry1..k
al., 2024b)
54.10%
48.36%
51.23%
STP-Lean (Dong Ma, 2025)
56.15%
Godel-Prover (Lin et al., 2025)
7B
pass 32 pass @
55.33%
DeepSeek-V3 (Liu et al., 2024)
685B
33.61%
Ours
DeepSeek-Prover Prover + LoT (whole-proof) PrepSeck-Prover MA-LoT
pass ( 128
62.70%
52.05%
57.42%
64 + 32 x 2 pass @ 32 16 8 x 2 cumulative
64.34% %
54.51 %
59.22%
Godel-Prover + LoT (whole-proof)
7B
57.79%
Godel-Prover MA-LoT
61.07 %
MA-LoT
65.98
63.93%
64.96 %
Table 1. Main experimental results of MA-LoT. Our results are presented as Base model method. The LoT (whole-proof indicates using the whole-proof results of our LoT-Solver model, and MA-LoT indicates the result of our whole pipeline. The sampling budget + k x in the MA-LoT framework indicates we first perform x whole-proof writing using the prover model and k rounds of correction using the corrector model. practice, one round of correction costs approximately half of whole-proof generation budget, resulting
the experiment process.
Method
Prover
round
round round
3.3. Results
DS-Prover-v1.5
51.64%
53.28
54.51%
55.33%
Godel-Prover-SFT
54.92%
59.43%
61.07%
61.89%
Table 1 presents main results, showing that MA-LoT achieves 61.07% accuracy rate on MiniF2F-Tess benchmark and 57.79% for LoT-Solver using whole-proof generation. After the enhancement of MA-LoT, we achieve 10.37% on Godel-Prover and 12.72% on DeepSeek-Prover on the MiniF2F- benchmark. This significant and uniform improvement of our framework indicates its effectiveness. Detailed analysis also shows that our models can solve IMO and AIME problems that previous models struggled with. Our model surpasses state-of-the-art tree-search (InternLM- 2.5) and whole-proof generation (Godel-Proved) baselines, demonstrating that our proposed model-collaboration frame- work based on Long CoT excels in formal theorem proving.
Prover us Corrector
54.92%
55.15%
57.38%
Table Results from multiple rounds correction using SeepSeek-Provert and Godel-Prover as base models, along with the outcomes of using prover to perform correction.
Method
MiniF2F-
NeepSeck-Prover-vL... (base model)
46.31%
LoT-Solver witch-off Long CoT w/o Long CoT training (on RI. model)
49.18%
48.36%
base model + Long CoT base model + Long CoT SFT
46.72%
50.00%
LoT-Solver
51.64%
MA-LoT outperforms all tree-search baselines by least 20.45% because its prover model constructs proofs with high-level NL planning using emergent Lean Long CoT reasoning capability. This indicates our prover model can leverage L.MMs strong NI. reasoning ability in its Long CoT, which leads to more comprehensive proofs. Additionally, MA-LoT surpasses whole-proof generation baselines by at least 10.37%, its corrector model analyzes, reflects, and reformulates proofs based Lean4 executor feedback in Long COT. The strong performance also demonstrates the ef- fectiveness of our ideas of integrating FL verification in NL
Table Ablation study result in pass@ 64 under DeepSeck- Prrooer Prover base model.
Method
Godel-Prover-SFT
MA-Lo'T-Godel
Sample budget
pass @:32
16 2 x
Avg. tokens gen
492.10
657.54
MiniF2F-Tee Test
58.20%
61.07% %
Table 4, Long CoT efficiency study result.

---

MA-LoT: Modcl-Collaboration Lean-based Long Chain-of- Thouught Reasoning enhances Formal Theorem Proving
Long COT reasoning with its emergent capability. Notably, the DeepSeek-Prover MA-Lo'T is based DeepSeek- Prover-vI.5-SFT; it outperforms its RL-trained variant by 6.15%. This suggests that our modellcoollaboration frame- work and Lean-based Long COT methodology align more naturally with formal theorem proving than RL alone.
3.5. Long CoTT Efficiency Study
To further study the property of Long CoT, we perform this experiment to test whether MA-LoT is able to search for the answer more efficiently. In this experiment, measure the GPU hours as well as the tokens generated in both MA-LoT and the base model. We observed that the MA-LoT generated 33% additional tokens and costs 70% additional GPU hours compared to the base model. Thus, to make fair comparison in the sense of computation hours, we enlarge the base model's sample budget to 1.7 times in this experiment; the results are presented in the Tab, 4. The table shows that despite having smaller sampling budget, MA-LoT still outperforms the base model by 4.93%, which indicates that MA-LoT is a better way to allocate computation power.
The comparison between LoT (whole-proof) and MA-LoT further highlights the importance of our modcl-collaboration framework. We observe 2.46% improvement by reallo- cating the computation resources from the prover model, which performs more whole-proof generation, to the cor- rector model, which analyzes and refines proofs based on Lean executor feedback. This validates the necessity of a model-collaboration system over relying solely on a prover model. In summary, these results confirm that Long CoT reasoning, combined with formal verification and a model- collaboration paradigm, enhances the discovery of non- trivial and in-depth proofs, thereby validating the effec- tiveness of our proposed method.
3.6. Ablation Study
To show the effectiveness of each component of our LoT-TI. training pipeline, we conduct this thorough ablation study, We demonstrate that the elements in LoT-TL pipeline work synergistically to strengthen the model's formal theorem- proving capability through integrating FL in Long COT. We use -arobeek---rv---1..... the pass @ 64 accuracy rate on the whole-proot prooff generation method for this set of experiments. The results are presented in Table 3.
3.4. Corrector study
To assess the impact of the correct model in MA-LoT, we present the cumulative accuracy on the MiniF2F-Test across different rounds of correction in Table for two of our base models. The prover column presents the pass@64 (or 16) accuracy rate of the prover model in whole-proof genera- tion, while Round-i columns indicate successive correction rounds. The results indicate that during the first three cor- rection rounds, the corrector model successfully corrects an average of 1 11.55 theorems that the prover cannot an- swer. Our analysis shows that most corrected proofs belong to IMO, AIME, and high-level MATH problems, which are particularly difficult for prior models. Such additional solved problems highlight the corrector's ability to analyze feedback from the Lean4 executor feedback using emergent Lean capability in Long CoT to discover non-trivial proofs. The case study for the analysis and regeneration of new proofs can be found in Section 3.7 and Appendix E.
as our base model and apply
3. EFFECT OF TRAINING STAGES
We evaluate training progression by measuring performance across key intermediate models, namely base model, base model Long CoT, and base model Long CoT + SFT, as shown in Table 3. Results indicate that training solely on NL CoT data provides minimal improvement. It suggests that the model lacks field-specific information to finish a com- prehensive Lean4 proof under pure general NL Long CoT training. However, incorporating SFT data with the LoT- Tl. training method yields a marked improvement, demon- strating the effectiveness of transfer learning in equipping models with Lean4 Long CoT capabilities. Interestingly, al- though it is not designed for whole-proof writing, additional training with correction data further enhances the perfor- mance. This improvement likely arises from the model's development of self- analysis capabilities in Lean4 code, allowing it to avoid potentially wrong solutions.
Additionally, to validate the effectiveness of the expert cor- rector, we conducted an experiment that used prover to perform corrections. In particular, we apply the LoT-Solver based on Goedel-Prover-SFT. We add the wrong Lean4 proof and error message as a comment in the Lean4 code block and ask the prover to correct it. Results are shown in the last row of Table 2. It shows a clear drop in performance in both correction rounds. This drop is because the prover model tends to directly repeat the wrong proof instead of using the Long CoT to analyze the error and correct the proof. This experiment shows the importance of expert corrector model, further validating the effectiveness of our idea of using FL as a backbone for Long CoT in NL.
3.6.2. SWITCH-OFF LONG CoT
This experiment shows that the strong FL reasoning power of LoT-Solver comes from the emergent formal reasoning ability in Long CoT, rather than trivially stacking more data. uses our LoT-Solver model to write Lean4 proofs directly using the code completion method without Long CoT. We find the performance drop from 51. 11.64% to 49.18%
8

---

MA-LoT: Modd--Collaboraioon Lean-based Long Chain-of- Thought Reasoning enhances Formal Theorem Proving
because the model does not take an explicit high-level plan in Long COT, making it unable to finish some questions in the induction field.
reasoning and multi-round thinking in Long CoT.
4.2. LLM Collaboration
Traditional RL methods offer training method solution for general reasoning and decision-making processes, but often suffer from low sample efficiency and generalization prob- lems (Pourchot & Sigaud, 2018). With the fast-developing reasoning and inttuuction-oolloiinn ability of LLMs, many researchers began to separate the cognition task for sin- gle LLM (Wang et al., 2022; Ma et al., 2024). The pri- mary method for the separation of tasks is to design special prompts and in-context examples let LLMs interact with the outsourcing tools using actionable responses (Xie et al., 2023; Yang et al., 2023). Further efforts were made to apply specialized training to enhance their field-specific capabil- ities (Xu et al., 2023; Reed et al., 2022). In the context of formal reasoning, most tree-search methods (Yang et al., 2024b; Lin et al., 2024; Wu et al., 2024a) apply an LLM to continuously query the executor and receive feedback to further refine the proof. Because of the huge difference between FL and NL, such methods are unable provide high-level analysis of the problem and provide a structured response.
3.6.3. ABLATION OF LONG COT
To validate the quality of integration between NL and FL in Long CoT, we fine-tune the DeepSeck-Provent Prover-v1.5-PP model directly using our SFT dataset without Long CoT reasoning. We can find that the performance of w/o Long CoT model (48.36%) is lower than LoT-Solver (51.64%). The results confirm that Long CoT plays a crucial role in Lean4 theorem proving, offering structured reasoning that outperforms a direct RL-based additional data fine-tuned model.
3.7. Case Study
This section presents the general results of case studies of the MA-LoT framework. Due to the limited space, we leave detailed examples in Appendix E. From the examples, we can observe a clear collaboration between models. The prover can use high-level plan to prove advanced MATH theorems, and the corrector can analyze the feedback from the Lean executor to formulate a correct proof of an IMO- level problem. The content in Long CoT also demonstrates the formal reasoning abilitics that emerge from our LoT- TL training pipeline in both prover and corrector. These observations qualitatively validate the coldelcollaboration system's 's design and emergence of formal reasoning ability in Long CoT, demonstrating its ability to combine high-level planning with iterative refinement in Lean-based Long CoT.
5. Conclusion
This paper introduces MA-LoT, comprehensive model- collaboration framework for formal theorem proving that leverages Lean- Long Thoouhhh (CoT) reason- ing. MA-LoT separate high-level proof planning from fine- grained correction, overcoming limitations of single-model approaches that either fail to harness LLMs' NL reasoning capability or lack integration with formal feedback. By coor- dinating a prover and corrector model through Long CoT, MA-LoT produces more structured, coherent, and insight- ful proofs. To support this framework, we introduce LoT-TL training-inference pipeline. This pipeline enables LLMs to develop domain-specnt ity through transfer learning without requiring specifically annotated Lean Long CoT data. We conduct extensive ex- periments on the MiniF2F benchmark, where the MA-LoT achieves 61.07% accuracy, surpassing all baselines, includ- ing both tree-search and whole-proof generation methods. These results highlight the value of combining formal veri- fication with structured and iterative Long CoT reasoning. Beyond theorem proving, LoT-7Z we proposed offers a general method for enabling Long CoT reasoning in other specialized domains without expensive RL. or data annota- tion. Additionally, the success of the model-collaboration Long CoT in Lean4 suggests broader applications of for- mal verification for enhancing structured reasoning across diverse fields.
4. Related Work
4.1. Lean4 Theorem Proving using LLMs
The application of LLMs for FL proving has been a hot topic for study in recent years. The tree-search including works represented by Expert Iteration (Polu et al., 2022), Re- Prover (Yang et al., 2024b), Lean-Star (Lin et al., 2024), and InternLMMSSeep-Prove (Wu et al., 2024b). This direction does not take full consideration of the LLMs' NL reason- ing ability and costs exponentially increasing computation power. Another direction treats formal languages as code and asks the LLMs to do the whole-proof generation without interaction with the Lean executor to fully use the NL reason- ing ability of LLMs. Significant works includes DeepSeek- Prover (Xin et al., 2024b;a), Theoreml (Wang et al., 2024), and Llemma (Azerbayev et al., 2023). Works in this direction tend to overlook the verification signals from Lean executors or do not thoroughly think about the error messages. Although there some early work (First al., 2023; Zheng al., 2023) that tries combine both models, it did not perform well because of the lack of thorough NL
Long CoT reasoning capabil-
9

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thougee Reasoning enhances Formal Theorem Proving
Impact statement
References
This paper presents work whose goal to advance the for- mal theorem proving using LLMs. The potential social im- pact majorly in the field of education. With the increasing number of formal languages used in graduate-level educa- tion, more advanced formal theorem proving model may result in educators being unable to distinguish the model- generated results and student writing results. Despite the societal consequences of improving formal reasoning sys- tems, specific discussions of ethical concerns are still too early at this stage.
Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F. L.,, Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al. Gpt-4 technical report. arXiv preprint arXi::2303.08774 2023.
Azerbayev, Z.,, Schoelkopf, H., Paster, K., Santos, M. D., McAleer, S., Jiang, A. Q.. Deng, J., Biderman, S., and Welleck, S. Llemma: An open language model for math- ematics. arXiv preprint arXiv:2310. 10631, 2023.
De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, The lean theorem prover (system description). In Automated DelluctionCAADE--2 Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
25th International
Dong, K. and Ma, T. Beyond limited data: Self-play Ilm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.0022 2025.
First, E., Rabe, M. N., Ringer, T. and Brun, Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium the Foundations of Software Engineering, pp. 1229-1241, 2023.
Frieder, S., Bayer, J., Collins, K. M., Berne, J., Loader, J., Juhász, A., Ruehle, F., Welleck, S., Poesia, G., Griffiths, R.-R., et al. Data for mathematical copilots: Better ways of presenting proofs for machine learning. arXiv preprint arXiv:2412.151884 2024.
Harrison, J. Hol light: An overview. In International Conference on Theorem Proving in Higher Order Logics, pp. 60-66. Springer, 2009.
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, Measuring math- ematical problem solving with the math dataset. arXiv 2021.
preprint urXiv:2103.0338
Jiang, Q., Li, W., Han, M., and Wu, Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378-392, 2021.
Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210. 12....222...... 2022.
Kumarappan, A., Tiwari, M., Song, P., George, R. J., Xiao, C., and Anandkumar, A. Leanagent: Lifelong learning for formal theorem proving. arXiv preprint arXiv:2410066009 2024.
10

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thoupe Reasoning enhances Formal Theorem Proving
Lin, H., Sun, Z.,, Yang, Y., and Welleck, S. Lean-star: Learn- ing to interleave thinking and proving. arXiv preprint 20t.24077.10400 2024.
Reid, M., Savinov, N., Teplyashin, D., Lepikhin, D., Lilli- crap, T., Alayrac, J.-b., Soricut, R., Lazaridou, A., Firat, O., Schrittwieser, J., et al. Gemini 1.5: Unlocking multi- modal understanding across millions of tokens of context. arXiv preprint arXiv:2403.05534 2024.
Lin, Y. Tang, S., Lyu, B., Wu, J., Lin, H., Yang, K., Li, J., Xia, M., Chen, D., Arora, S., and Jin, C. Goedel- prover: A frontier model for open-source automated the- orem proving, 2025. URL https://arxiv... org/ abs/2502 07640.
Shao, Z., Wang, P., Zhu, Q. Xu, R., Song, J., Bi, X., Zhang, H., Zhang, M., Li, Y., Wu, Y., et al. Deepseekmath: Push- ing the limits of mathematical reasoning in open language models. arXiv preprini arXiv:2402.03300 2024.
Liu, A., Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng, C., Zhang, C.,, Ruan, C., et al. Deepseek-vy v3 technical report. arXiv preprint vmXiv:2412.1943/ 2024.
Wang, R., Jansen, P., Côté, M.-A., and Ammanabrolu, P. Scienceworld: Is your agent smarter than a 5th grader? arXiv preprint arXiv:2203.0P
2022.
Ma, C., Zhang. J., Zhu, Z., Yang, C., Yang, Y., Jin, Y.,
Wang. R., Zhou, W., and Sachan, M. Let's synthesize step by step: Iterative dataset synthesis with large language models by extrapolating errors from small models. arXiv preprint urXivv23100 13671, 2023.
Lan, 7., Kong, I.., and He, J. Agentboard: An analytical evaluation board of multi-turn Ilm agents, arXiv preprint arXiv:2401. 13178 2024.
Moura, L. d. and Ullrich, S. The lean 4 theorem prover and programming language. In Automated Deduction- CADE 28: 28th International Conference Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Wang, R., Zhang. J., Jia, Y., Pan, R., Diao, S., Pi, R., and Zhang, T. Theoremllama: Transforming general-purpose Ilms into lean4 experts. arXiv preprint arXiv:240..03203, 2024.
Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F,, Chi, E., Le, Q. V., Zhou, D., et al. thain-of-thoughh prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824-24837. 2022.
Newell, A. and Simon, H. The logic theory machine-a com- plex information processing system. IRE' Transactions on information theory, 2(3):61-79, 1956.
Open-Source-O11 Open-ol, 2024. URL https:// github. wwwm www.raoooooeeeeoeeeeeeeeee Ac- cessed: 2024-12-28.
Wu, Z., Huang, S., Zhou. Z., Ying, H., Wang, J., Lin, D., and Chen, K. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration large-scale lean problems. arXiv preprint arXiv:2410. 15700, 2024a.
OpenAl. llms.
to reason with https: /ttp:///p///a./////e /tt.li.ooo///e/////eeeeeeeeeeeee / sorninngttorrasseee with-ih 1lma/ / September
Learning
Wu, Z., Wang, J., Lin, D., and Chen, K. Lean Lean-githubl Compiling github lean repositories for versatile lean prover. arXiv preprint
13 2024. Accessed: 2024-11-24.
2024b.
Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994.
Xie, T., Zhou, F., Cheng, Z., Shi, P., Weng. L., Liu, Y., Hua, T. J., Zhao, J., Liu, Q., Liu, C., et al. Openagents: An open platform for language agents in the wild. arXiv preprint arXiv:2310. 10634, 2023.
Polu, S. and Sutskever, I. Generative language model- ing for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
Xin, H., Guo, D.,. Shao. Z., Ren, Z., Zhu, Q., Liu, B., Ruan, Li, W., and Liang, X. Deepseek-prove Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405. 14333, 2024a.
Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematies statement curricu- lum learning, arXiv preprint arXiv:2202.01344, 2022.
Pourchot, A. and Sigaud, O. Cem-rl: Combining evolution- ary and gradient-basse based methods for policy search. arXiv preprint arXiv: 022,, 2018.
Xin, H., Ren, Z., Song. J., Shao, Z., Zhao, W., Wang. H., Liu, pprseekk-roove--ll.
B., Zhang, I.., Lu, X., Du, Q., et Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.0811 2024b.
Reed, S., Zolna, K. Parisotto, E., Colmenarejo, S. G., Novikov, A., Barth-Maron, G., Gimenez, M., Sulsky, Y., Kay, J., Springenberg. T., et al. A generalist agent. arXiv preprint wrXxx:220506/777 2022.
Xu, Y., Su, H., Xing, C., Mi, B., Liu, Q., Shi, W., Hui, B., Zhou, F., Liu, Y., Xie, T., et Lemur: Harmonizing

---

MA-LoT: Modcl-Collaboration Lean-based Long Chain-of-Thoughl Reasoning enhances Formal Theorem Proving
natural language and code for language agents. arXiv preprint arXiv:23/0.0663 2023.
Yang. H., Yue, S., and He, Y. Auto-gpt for online decision
making: Benchmarks and additional opinions. arXiv 2023.
preprint arXiv:2306.0222
Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A new frontier ai. arXiv preprint arXiv:2412.1607 16075, 2024a.
Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Leandojo: Theorem proving with retrieval- -aumeeted language models. Advances Neural Information Pro- cessing Systems, 36, 2024b.
Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set for- malized from natural language math problems. arXiv preprint arXiv:2406. 0084770..37.... 2024.
Zheng, C.. Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. Lyra: Orchestrating dual correction automated theorem proving, arXiv preprint 1rXiv:2309.15806 2023.
Zheng, K., Han, J. M., and Polu, S. Minif2f: cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.0011 2021.
12

---

MA-LoT: Modd--Collaboration Lean-based Long Chain-of-Thoupe Reasoning enhances Formal Theorem Proving
A. Term chart
Training Steps
MiniF2F-Tess
To make the reader better understand the terms, we pro- vide this chart that explains every term, abbreviation, and corresponding tool in detail.
125 Steps
32.79%
250 Steps
35.25%
1,250 Steps
45.08%
2,500 Steps
47.54%
13,616 Steps (full fraining)
51.64%
1. NL (Natural Language): Refers to language that hu- mans use in our daily life, often unable to perform auto-verification.
Table 5, MiniF2F-Test result different data-scale trained models
B. Examples for tree-search and whole-proof generation
2. FL (Formal Language); A structured and mathemati- cally precise representation of logic and proofs, which ensures rigorous verification and eliminates ambigui- ties present NL reasoning.
Following Section 2.1, we present the input-output example for tree-search method and whole-proof generation method here.
3. Lean4: A functional programming language and in- teractive theorem prover developed for formalizing mathematics and verifying proofs.
Example for whole-proof generation:
+*# Input Example
Complete the following Lean 4 code: theorem algebra algebra_sqiine unt..utaccccireeabblllll
4. Lean Executor:
The built-in proof verification engine of Lean4. evaluates proof steps, checks for correct- ness, and ensures that every logical inference follows strict formal verification rules.
(a b: R)
(ho : a"2 b
a b (a - b) $ 1 : by
#* Output Example
-- Me have that (a b - 12 2 0. 11
5. Long CoT (Long Chain-of- Thain-of-Thoughty: The reasoning structure provided by OpenAI-O1 (OpenAl, 2024) that performs long and detailed thinking before making the final output. Different from standard CoT, Long CoT allows for multi-step logical reasoning before proof generation, reflection, and iterative refinement from self-check of Lean4 feedback.
have sq_neneeg
S (a
-- By expanding, we have:
-- 0 < a -ab-a-abtb" 22 +b-a+b+1.
1inarith [ho,
a b]
Example for tree-search method:
+# Input Example DECL MyNat.mul GOAL b n + (a b) ~n -n-a ** Output Example PROOFSTEP induction with Ht
6. MA-LoT (Model-CollAAbration Lean-based Long Chain-of-Thought framework); Our proposed model- collaboration framework for formal theorem proving.
7. LoT-TL (TonsTransfer Learning): The transfer learn- ing pipeline we propose enable LLMs with Lean4 Long CoT capability without the need for a specially annotated dataset.
C. Scaling Law Study
We conduct an additional experiment to investigate whether model adheres to scaling laws by evaluating its perfor- mance across varying training dataset scales. Specifically, we train the model with four distinct step sizes (125, 250, 1250, and 2500 steps) under a fixed batch size of 4 and evaluate its accuracy on the MiniF2F- Fest benchmark using the Long Chain-of-Thought (CoT) format. The resulting accuracy rates are presented in Table 5. To analyze these results, we plot the relationship between log-scaled training steps and model accuracy in Figure 3. A linear approxima- tion of the data yields strong coefficient of determination (R²2 0.9664), indicating a mear-lineat improvement in performance as training steps increase logarithmically. This aligns with the predictions of scaling laws, suggesting that our approach benefits significantly from larger-scale train-
8. LoT-Solver: The model we train through LoT-TL pipeline that serves both as prover and corrector. It is high-standard Lean4 theorem proving model with Long CoT capability to control the type of cognition task and enhance formal thinking.
9. LoT-PD & LOT-CD (LoT-ProveData) & (LoT- CorrectionData): The LoT-PD a dataset containing verified Lean4 theorem proofs and NL statement and proof. Its main function is to provide basic capability for the prover. The LoT-CD is a dataset containing incorrect error messages and correct Lean4 proofs to- gether with NL annotations. mainly provides the capability for the prover model to refine proofs.
13

---

MA-LoT: Moddl-Collaboration Lean-based Long Chain-of- Chain-of-Thought Reasoning enhances Formal Theorem Proving
Scaling Law Study
R 0.9664
Accuracy Rale
64
Log Segg-Sclle"Te Training Steps
Figure 3. Log-scale training steps and accuracy rate MiniF2F of trained model. The dashed line linear regression approxima- tion.
ing. Our findings further highlight the potential for enhanced performance with expanded resources to annotate additional Lean4 data.
D. ProofNet result
We perform a small-scale baseline comparison on the ProofNet benchmark using the Goedel-Prover-SFT and MA- LoT(Goedel), where MA-LoT achieves 15.47% of accuracy rate under 16++16 16 metric while the original Poodel--roverr is 12.15% under pass @32. The relatively low performance of both models is that Goedel-Prover does fit the ProofNet well as reported in Lin et al. (2025). However, see the improvement of our method compared to the base- line, indicating MA-LoT's effectiveness is not constrained to the baseline.
still
E. Case studies
We present two studies in Appendix E.1 and E.2. We see that the model-collaboration framework can write more coherent and well-structured proof by making high- level NL plan and executing such a plan in the prover. The corrector can analyze the unsolved goals, make plans for correction, and write correct proof. This is achieved by our proposed training procedure.
14

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
E.I. Prover analysis
This is an example of prover-generated result, in which can see that the prover model learns write high-level proof plan in the Long CoT and details execute the plan when writing the Lean4 code
### Provided Long CoT Header <Thought>
Alright, I should do the following:
1. Provide the natural language analysis for the theorem based on the Natural
- language theorem statement.
2. Draft the Lean4 tactics should use to solve the problem
3. Write the output Lean4 code.
The user also asks that should avoid using the keyword "sorry" give up the proof, ### Generated results:
will not write it in my Lean4 code.
The hoanoet_oombeerooy___55. can be proofed by leveraging the properties of
4 modular arithmetic. Specifically, we know that if "n & 8 = 7", then "n" can 4 be expressed as "n 8k 7' for some integer 'k' We need to find 'n $ 4" First, observe that 'n
7" Since "8k" divisible by 4 '4", we only need to consider the remainder when '7' divided by '4", which 4 is "3". Therefore, "n & 3"
7" implies
Now, translating this reasoning into Leand code, can the properties of modular arithmetic to directly derive the result.
</Thought> <uupput> .. "lean4
theorem mathd mathd_ wwwbertteery_.55.5.
: N) (ho n 7) n 4 :- by We know that leaves remainder of when divided by 8. have h1
8 8 7 hg We need to find the remainder when is divided by 4.
have h2 n & 4 = 3 :- by -- Using the fact that divides 8, we can use the modulo operation - properties.
rw [+ Nat mod_modd mod of dvd n (by decide
8)
Simplify the expression using the given remainder when divided by 8. simp [h1]
Therefore, the remainder when n is divided by 4 is 3.
exact h2
</Output>
E.2. Corrector analysis
This is an example of error correction that successfully solves an IMO problem, We can see that the model first analyzes the emor message, then makes a proof plan, and then writes a correct proof for another IMO-level problem
### Provided Long CoT Header <Touugh>>
Alright, need to prove the theorem prover_data 63499 using the Lean4 code. Here is my draft of the proof:
leenn theorem [mo__9833_p0 (a b c R) (he 0 C)
15

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of- Thoughht Reasoning enhances Formal Theorem Proving
(h1
a
(h2
a c)
(ha
<
b
+
0
S
a²2
+ (a - b) + b * (b c) + c (c - a) = by
/-
To prove that \( a ( b) 2 cb c) c a a) \eeg 0 \) for
- positive real numbers (( a V, \( V), and \ a \ satisfying certain conditions related to being part of triangle, we can proceed as follows: 1. **Nonlinear Arithmetic**: Utilize nonlinear arithmetic ('nlinarith") to verify inequalities involving squares and products of differences between variables. These operations inherently handle cases where expressions mi ght not hold due to cancellation or sign changes.
Equality holds if all pairwise differences among (( a W,, A W, and \ V)
- become zero simultaneously, However, since they must satisfy strict positivity constraints imposed by "triangle", such an eventuality cannot
occur under normal circumstances unless specified otherwise. Nonetheless,
within the confines of algebraic manipulation without additional constraints beyond those provided, no immediate contradictions arise regarding potential zeros leading to equality.
-/
Introduce intermediate hypotheses ensuring divisibility properties do not - disrupt expected behavior. have ha' True trivial have hb' True trivial
have he! True := trivial
Employ nonlinear arithmetic to iteratively check for inequalities involving
- sums and products of our main variables and constants.
repeat' nlinarith [mul_pos hg.1 hg.2.1, pos_ h0.2.1 2.. pos 2..2.2 1g.
sub_ jub_self a, sub
sub_sell self b, bub_sell c, add sub cancel' paacell_rrghht right a b,
sud_sub_cancel' _rrght rrrgght b c, did_suubcancel_rit
a, mul_nonneg (ha', .1e) (hb' ,1),, mul_nonneg (hb .1e)
(he'.le))
mul mul_nonneg (he', le) (ha'.le)) .l)]
Let me test it in Lean4 Emmm, it seems the above proof is wrong. Let me check the error messages.
OK, Here is the error messages: **bash line 13
unsolved goals b g
ho a 0<bb0<e
h
b
h2 : <b<at c
ha ta<b c
ha hbd he' True
FO
* (a b) b - 2 (b c) * a + (c a)
>>g
So, will rethink a Leand proof following the steps
16

---

MA-LoT: Modd-Colllaoortionn Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
1. Provide the natural language analysis for the theorem based on the Natural language theorem statement, Lean4 theorem statement, my previous proof and the error message.
2. Draft the Lean4 tactics I should use to solve the problem
3. Write the output Lean4 code.
Let me analysis the wrong Leand solution through the error messages, ### Generated results"
The error message indicates that the proof incomplete. The error message says:
unsolved goals
b c R
ho : 0 a A 0 <bbosc
h : c a b
h2 : :
c
ha : ba<b c
bakbb+
ha' hb' he' True
Fosa
b * (a b) + b 2 (b - c) a 2 (c a)
So, the main issue is that the proof is incomolete, and the final goal 0 S a *
4 b* - b) b * c (b c) + e²2 a (c - a) is not being addressed
- properly.
Therefore, need to construct a proper proof strategy that addresses all the conditions and goals properly.
First, I need to understand the mathematical structure of the inequality "a"2 b (b - c) + c"2 This expression is symmetric in "a", "b", and 'c' Given that 'a', "b", and "c" are positive real numbers and they satisfy certain - conditions related to being part of triangle (triangle inequalities), can think about the properties of such expressions.
* (a b) + b
(c - (a-
One appreach is to conaider the symmetry and positivity of "a', 'b,, and 'c' Since 'a', "b', and "c" are sides of triangle, they satisfy the triangle inequalities:
-aa + c²
-b > b'
Additionally, since 'a', "b,, and "c" are positive, we can use properties of real prove the desired result. Another approach is to use algebraic manipulation or inequalities like AM-GM inequality or Cauchy-Schwarz inequality.
numbers and inequalities
Given the complexity of the expression, perhaps rearranging terms or applying known inequalities could help.
Also, considering the conditions of the triangle, perhaps expressing the 4 variables in terms of each other or using substitution could simplify the 4 problem.
need to ensure that the final proof is logically sound and does not rely assumptions that are not justified. Therefore, I will proceed to construct a revised proof based on these + considerations.
Let me proceed with the thought process and output the corrected Lean4 code. </Thought>
<Output> llenn
17

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thoughl Reasoning enhances Formal Theorem Proving
-- Let $a5, $b$, and $c$ be the lengths of the sides of triangle. Prove that $a"2 (a b) b-2 (b e) c² ( a) Ngeg O$.
-/
theorem imo _1___193_____ (a b c R)
(ha 0 < A 0 < b <bao<o
(hi c c < b)
(h2 b < c)
(h3 <
0 a b (a b) b'2
(b c) + c02 (c - a) by
-- We will use the fact that the square of any real number is non-negative.
have h4 0 < (a b) :- sq_nonneg (a - b)
have h, 0 S (b c) := sq_nonneg (b - c)
have he 0 S (c 2 := sq_nonneg (c a)
Using these inequalities, we can conclude the desired inequality using
non-linear arithmetic.
nlinarith [mul_ hg.1 hg 2..2.1, mul pos 2..2.1 hg 2.2, mul pos pos 2.2 ho 1, (sub_pos.mpp h2), mul_pos (sub_pos mpr h2)
mul_pos (sub_pos mpr mpr h1)
(sub .ppr h3), pos (sub_pos pos.mpr
mpr ha) (sub_pos.mg h
</Output>
Another example demonstrated as follows:
Natural language theorem statement:
mathd_algebra__
What is the value of S-a-b"2+3abs if $a=-1$ and $b=5$? Show that it is -39.
Lean4 theorem statement:
>> 1ean4
theorem mathd_algebra_4119
b : R)
(ho
-11
(h1 b = 5)
-a - b22 + (a * b) = -39 : by
Lean4 theorem statement and proof with explanatory comments precedi ng each line
of code:
### Response:
<Thought>
Okay the user asks me to write Lean4 theorem proof using Long CoT, I should do
+ the following:
1. Provide the natural language analysis for the theorem based on the Natural language theorem statement.
2. Draft the Lean4 tactics I should use to solve the problem
3. Write the output Lean4 code.
18

---

MA-LoT: Modd-Colllboortionn Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
The user also asks that should avoid using the keyword "sorry" give up the a proof, will not write it in my Lean4 code.
The natural language analysis for the theorem 'mathd mmathd_aggebra, algebra__199 is:
Given a -1 and b 5, we need to compute the value of the expression -a b² +
3ab and show that it equals -39.
The steps to solve this problem are:
1. Substitute = =1 and b = 5 into the expression.
2. Simplify the expression step by step.
3. Verify that the result is -39.
The Lean4 code for this theorem would involve substituting the given values for a and b into the expression and then simplifying it using algebraic operations.
+
Now, let 's outline the Lean4 code:
The theorem statement is:
theorem mathd_algebba__e 419
b : R)
(ho
-1)
(h1 b = 5)
-a - b + 3 (a + b) = -39 := by
The proof would involve substituting the values of a and into the expression a and simplifying:
First, substitute -1 and 5 into the expression:
-a - ba + 3ab becomes:
((1) - (5) (-1)
Simplify each term:
-(-1) =
25) = -25
3x (-1) (5) -15
the expression becomes:
1 25 - 15
Now compute the result:
25 -24
-24 -15 -39
19

---

MA-LoT: Modc-Coollaboratoon Lean-based Long Chain-of-Thoughe Reasoning enhances Formal Theorem Proving
Thus, the value of the expression is -39.
Now, let's write the Lean4 code.
The code would start with the theorem statement, then use the "rw" tactic to + substitute the values of a and b.
Wait, but in Lean4, we can directly substitute the values into the expression. So the code would be:
theorem mathd_algebra___ _49
(a b : R)
(ho a -1)
(h1
5) :
-a +
-39 by
rw [ho, h
ring
But wait, 1et me check. The expression is -a b + 3ab. So substituting a -1 a and
(-1) - 5 (-1) = -25 -15 -39.
Yes, that's correct.
So the code can be written as:
zw (hor h1]
Then use the "ring" tactic to simplify the expression.
So the complete code would be:
theorem mathd_algebra__a
b :
(ha
-1)
(h1 b = 5)
-a - b22 + (a + b) = -39 := by
rw [hor hil ring
Alternatively, using the "simp" tactic with the appropriate lemmas.
But in this case, the 'ring" tactic is sufficient.
So the code is straightforward.
should test this code in Lean4 to ensure that it works.
But since the user asked to avoid using 'sorry', will not write the code. Instead, will provide the explanation.
20

---

MA-LoT: Moddl-oollaboration Lean-based Long Chain-of-Thougee Reasoning enhances Formal Theorem Proving
</Thought>
<Output>
To solve the problem, we need to evaluate the expression ((-a - b + 3abl) given
- (a -1 and \ (b 5, and show that the result is \(-39))
#*# Key steps:
1. Subssiittte the given values into the expression:**
Replace (a\) with \--1) and \ (bb)) with (5V)
The expression becomes (--(1) - (5) 22 3 (-1) (5) V.
2. **Simplify each term:**
\(-(11) 1V)
2 251)
(-3 (5) 115)
3. C*Combine the simplified terms:** \11 - 25 15 -39))
### Proof:
"lennn
theorem mathd_algebra_At _19
(a b R)
(ho = -1)
(h1 b = 5)
-a - b + 3 (a * b) = -39 = by
rw [ho, hil
ring
### Explanation:
++Substitution:* The 'zw [ho, hi]' tactic replaces (al) with ((-1)) and \bb) - with (51) in the expression.
**Simplification: The "ring" tactic simplifies the expression using algebraic - rules, resulting in (-33)).
This approach ensures that efficiently and correctly evaluate the expression by substituting the given values and simplifying step-by-step The final result confirme rms that the value of the expression is indeed (--39)) </Output>
From the example above, can clearly the saying of wait, which indicates rethinking process of the Long CoT. Such rethinking can help the model to reach conclusion that needs more thorough thinking.
E.3. Theorem only solved by MA-LoT
We have observed that algebra,2varling ceaelinneree_ffp3zeeee [.3.fmmmmzequde weeeeeegge1e00ee is only solved in the MA-LoT setup. From the original code draft and the error analysis, we can spot that our corrector framework is able restructure the proof from the previous left and right cases into direct solving. This indicates our method's superiority in rethinking based on formal guidance.
<Thought>
Alright, I need to prove the theorem code. Here is my draft of the proof:
68493 using the Lean4
21

---

MA-LoT: Modd-Colllbooraionn Lean-based Long Chain-of-Thonn Reasoning enhances Formal Theorem Proving
leann import Mathlib
import Aesop
set_option maxieartbeatts
open BigOperators Real Nat Topology Rat theorem algebra wetpa_/aaaallaaaeee htgparr___aaaeeeeee____eeee_aaa htt.ff/eeee....ffmmimeeeeeeeeee 1eanaee0e__e11_0____
(f z: C)
(he f 3+z = 11)
(h1 3f - 1) - -5z - -6)
= A 2
:= by
Given the equations \(
11 and A 3f show that A( -10 V) and \ z A).
-68 V), we need to
1. Start by isolating \ f \) from the first equation: A( f 11 32 V
2. Substitute \( f 11 - 3z A) into the second equation: A 3((11 - 3z) 1) -
5z = 68 \)
3. Simplify the equation step by step:
Distribute the 3: 3 (10 32) 52 -68 W
Distribute the 3 again: A 30 92
-68 V).
Combine like terms: \( 30 14z -68 V.
4. Solve for \( A):
Subtract 30 from both sides: \( -14z = -98 W.
Divide both sides by -14: \< 2 = 7 V.
5. Substitute (( z 7 back into \ f = 11 3z \):
(( 11 ((7) V.
( 11 21 M.. -10 V.
1( f -10
Thus, have shown that Al -10 and A W).
-/
constructor case left =>
-- Isolate from the first equation have h2 : f
3xz := by iinear_combination ho
Substitute into the second equation
have 3* (11 3*2 1) 5+2 -68 by [hg] hii exact h
Simplify the equation to solve for
have h4 30 - 14+z -68 = by linear_comt nation hg
have hş : -14xz -98 :- by linear cntterr_cobinntiiin h4
have hg : 2 = = by linear_combinate combination hş / -14
exact he
case right Isolate from the first equation by
have he
exact h2
Let me test it in Lean4
Emmm, it seems the above proof is wrong.
Let me check the error measages.
22

---

MA-LoT: Moddl-Collaboration Lean-based Long Chain-of-Thoonee Reasoning enhances Formal Theorem Proving
OK, Here is the error messages:
""aaash line 39
type mismatch h6
has type = 7 Prop
but is expected to have type
f - -10 Prop
"bbbhh line 42
ring failed, ring expressions not equal
f z : C
ho : f
* 2 = 11
h : 3 (f 1) 2 -668
+ + (- 2) f)
So, I will rethink a Lean4 proof following the steps
1. Provide the natural language analysis for the theorem based on the Natural language theorem statement, Lean4 theorem statement, my previous proof and the error message.
2. Draft the Leand tactics should to solve the problem
3. Write the output Lean4 code.
Let me ana analysis the wrong Lean4 solution through the error messages
The first error says:
line 39: type mismatch
he has type 2 = 7 Prop but is expected to have type f = -10 Prop
Wait, in the code, I have two cases: left and right. The left case is supposed to
+ prove f -10, and the right case z 7. But in the left case, derived z
7 and then tried to use he to conclude f -10, but he is 7. That's the type mismatch. So, I need to fix that.
The second error is:
line 42: ring failed, ring expressions not equal
C
23

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of- Thought Reasoning enhances Formal Theorem Proving
ho f
h1 3 (f - 1) - 55 x = -68
+ (- * 2) f) =
Hmm, this seems like an unrelated expression that Lean is trying to check. Maybe - there's mistake in how I'm handling the substitutions or the algebraic manipulations.
Let me revisit the code. In the left case (proving f = -10), I first derived f = 11 - 3+z from ho, then substituted that into h1 to get h3. Then I simplified hy to get has has and ha, which led to 2 = 7. But then tried to use h& to -10, but hg is z 7. I need to instead use z to find
- conclude
so, in the left case, after getting z 7, should substitute that back into f 11 3+z get f = -10. Then I can that to conclude f -10.
similarly, in the right case, I need to properly handle the substitution and - simplification steps to avoid the ring error.
Let me try adjusting the code accordingly. Instead of having separate cases for left and right, maybe should first solve for z, then use that solve for E, and then combine the results. Let's see how the corrected code does it. </Thought>
<Output> "lean
import Mathlib
import Aesop
set_option maxHeartbeats
open RigOperators Real Nat Topology ogy Rat
/--Given that 32 11$ and (f 5z -68$, show that $f -10$ and $z
7$ theorem bttpphah.aaaaiieeeeeeeeeeeeeeeae
(f z: C)
(ho f 3+z = -11)
(h1 (f - 1) - -52 -68)
-10 A z
== by
/-
Given the equations \( 3z 11 and \ 3f
5z -68 \), we aim to
show that \( -10 \) and \ 7 \).
1. Start by isclating A f \) in the first equation: \( = 11 - 3z \).
2. Substitute \( f 11 - 3z A) into the second equation: A( 3 - 3z 1)
- 52 = -68 \).
3. Simplify the equation step by step:
Expand the terms inside the parentheses: \( 3(10 32) 5z -68 \)
Distribute the 3: \( 30 9z 5z -68 V).
Combine like terms: \( 30 14z -68 \)
4. Solve for \ \):
24

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
Subtract 30 from both sides: A -14z -98 V). V. Substitute ( = 7 V back into (( f = 11 - 32 A): Calculate A f M): A f = 11 - (7) = =11 - 21 = -10 V)
Divide both sides by -14: ( z
5.
6. Conclude that A f -10 V) and ( 2 = V.
-/
Isolate in the first equation have h2 :
3+z := by danear_combinatinn ho
Substitute
11 3z into the second equation
have ha 3x (11 - 3+z 1) 5xz -68 by rw [h2] at his exact h
Simpli fy the equation step by step
have h4 3+10 - 9+2 5+z - -68 : by direar_combinate h3
have hs 30 - 14+2 -68 = by
h4
Solve for z
have he -14*z -98 :- by dinear_combinate hş
have h7 z = 7 := by linear_combination
he -14
Substitute
7 back into f 11 32
have h8 f = -10 := by rw [h7] at h2; linear linear_combe combinaiiinnnnnn h2
-- Conclude the proof exact (hg, b7)
</Output>
F. Training examples
This section, we present the training examples for SFT data and correction data. We can see that in the LoT-TL. training stage, we keep the system prompt to switch off the Long CoT thinking. particular, in the SFT data, we switch off the entire Long CoT., In the correction data training, we only switch off the analysis of error messages in the Long CoT while providing the error message well the original proof draft as a component in the Long CoT.
F.1 LoT-TL Training example for SFT data
Input Example
<bbegin_of_sentence >You are a helpful assistant who will solve every problem **TTHOU Long Chain-of-Thought
### Instruction:
@ Natural language theorem statement:
prover_data_298:
This all simplifies to: $55r33(55+35) (12"7}
e Lean4 theorem statement:
"eleea4
theorem anoovr_ddta__20 298
((55 35) / (1277) @) = (55 35) / (1277) by
0 Lean4 theorem statement and proof with explanatory comments preceding each
line of code:
**# Response:
Output Example
<hougght>
The user ask not to solve with long CoT, I will directly write the answer. </Thought>
<Output>
... 1eaa4
---This all simplifies to: $15rac(55*35) (1277)8-/
theorem prover_data_ 298
25

---

MA-LoT: Modd-Colllbooraionn Lean-based Long Chain-of-Thouge Reasoning enhances Formal Theorem Proving
((5 35) (1277) -Q- (55 35) / (1277)
by
/-
To prove that \(fracc55 Acdot 35) (12(11271) (1 is equal to \(ffacc(55 Vcdot (12"7))) we simply observe that the expressions on both sides of the equality are identical. This identity holds true because the numerator and denominator are the same on both sides.
use the fact that the left-hand side and the zight-hand side the equality are the same.
congr
Simplify the power expression.
<;> simp [pow_succ]
Normalize the numerical values to confirm the equality.
<;> norm_num
</Output>< end_ of
E2. LoT-TL Training example for correction data
Input Example
<lbegin_of_senteneee | >>Yuu are helpful assistant who will solve every problem **WITH** Long Chain-of-Thone Thought. You can make some Lean4 proof draft in your 01 style Long internal Chain of Thought (CoT) and you have the ability to test the thing during your thinking. You need to use the error messages your Long COT to guide your proof generation but you are required **NOT** to provide natural language analysis to the errors. 4h Instruction:
@ Natural language theorem statement:
prover_data_221e
Given negatiee real numbers $a, b, c$ with $a + + + toc 1s. Prove that:
$7 (ab be + ca) \leq 2 9abo$.
Lean4 theorem statement:
leenn
theorem prover_data_21 (a b c : R) (ha 0 (hb 0 b) (he : 0 < c) +
(habe + b 1) (a b
V
2
:= by
0 Lean4 theorem statement and proof with explanatory comments preceding each
4 line of code:
4#$ Response:
<Thought>
Alright need to prove the theorem prover_data_211 2216 using the Lean4 code.
Here is my draft of the proof:
leann
theorem
2216 (a b a : R) (ha : 0
a) (hb 0 S b)
(hc : :0 0 c)
+ (habe a + b + +cc 1) 1 (a babb
a)
axba
:= by
with aes
..g
Let me test it in Lean4
Emnn, it seems the above proof is wrong.
Let me check the error messages.
OK, Here is the error messages: t*abash
26

---

MA-LoT: Modd--Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
line 7 unexpected token 'with'; expected '(' tactic
'*
""bashh
line
unsolved goals
a b c : R
ha : < a
hb 0 < b
he : ::00
habc a b
+7* * (a b b
+ x
Output Example
Since the user ask NOT provide natural language analysis to the problem. Let directly try write the revised code.
< <Touchh>>
<Output>
"eann
/ --Given non-negative real numbers $a, b, c$ with $a c 18. Prove
+ that: $7 + be + ca) \ieq 2 + 9abc$.
theorem prover_data_ao 2216 (a a : R) (ha 0 0 a) (hb S b) (he : 0sc
(habe a 1)
(a b baxbbbacton al 1
2
by
/-
Given non-negative real numbers \a)), \bb), and (cl) such that (aa + b +
c = 1\), we need to prove that \77 (ab + be + ca) Vleq 2 + 9abe)). The
proof involves using algebraic manipulations and inequalities to show
that the left-hand side is bounded above by the right-hand side.
Specifically, we use the fact that squares of real numbers are
non-negative, which helps in establishing the required inequality.
Normalize the expression involving 'a', "b', and "c" to prepare for a algebraic manipulation.
ring_nf at habe +
Use 'nlinarith" to handle nonlinear arithmetic inequalities. This includes checking non-negativity expressions involving "a', "b" and
"c'.
nlinarith [sq_nonneg (a 1), sq_nonneg (b 1), sq_nonneg (c - 1), sq_nonneg (a - b), sq_nonneg (b c), sq_nonneg (c a)
nonnen (a + b + c]]
27

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
G. Models input example
G.1. Prover model input-output example
### Input Example
IMO problem our prover found
@ Natural language theorem statement:
imo_1961_p11
(' ("Hungary"')
Solve the system of equations:
<center>
$
Abegin (matrix)
Aquad y \11 &= 1; , II
x +y"2t2"2 \ll &=b 11
Aqquad \qquad xy 111 6= z'2
(entriitrix)
</center>
where Sa and $b $ are constants. Give the conditions that $a and $b $
must satisfy so that $x, y, $ (the solutions of the system)
distinct positive numbers.
e Lean4 theorem statement: 1ean4
theorem imo_ [mo_1961_pl (x y b R) (be
x A < y N 2) (h1
x * y)
(h2 : y # z)
(h3 # x)
(hĄ
y + a) (hs 2 + y
2 2
2 b 2) (he
y - 2)
0 < A b 2<a 2 2 := by
0 Lean4 theorem statement and proof with explanatory comments preceding each
line code:
Response:
<Thought>
Alright I should do the following:
1. Provide the natural language analysis for the theorem based on the
4 Natural language theorem statement.
2. Draft the Lean4 tactics I should use to solve the problem
3. Write the output Lean4 code.
The user also asks that should avoid using the keyword "sorry" to give up the proof, so I will not write it in my Lean4 code.
### Output Example
The "imo_ 'imo_1961_p1" can be proofed by analyzing the given equations and deriving necessary inequalities to ensure that the solutions are distinct 4 positive numbers.
</Thought>
<Output>
leann
theorem imo_ _oo_1961_p1 b R) (ho 0 SYYO 2) (h) x # y)
(h2 : + 2)
28

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thone Thought Reasoning enhances Formal Theorem Proving
(h3 z # x) (h4 x
a) (hş 2 y
2 b 2) (hg
y
2)
0 < aal b 2 < a < 2 := by
-- We need to prove three inequalities: 0 < 2 a²2, and a < 3 b*2.
refine' (,
First, prove 0 < a.
Since x, y, 2 are positive, their sum a must also be positive. nlinarith [hp-1, hg. hg 22. nonnen (x y) sqnnonneg ( 2),
sq_nonneg (z x)]
Next, prove b < a*2.
-- Using the given equations and inequalities, derive the necessary inequalities.
nlinarith (mul_self_pos.meg mpr @sub_ne_zero.nee mpr h1), mul mul_self_pos mpr ctub_ne_zerg mpr h2),
mpr (sub_ne_zero) pero. mpr ha), nonnen (x y), sg_nonneg (y mul_self_pos mpr
2), sq_nonneg (2 x)
Finally, prove a²2 3 b
Combine all the given information to derive this inequality. nlinarith [mul_self_pos.m] hg),
h1), mul_self_pos_ mpr
mul mul_self_pos mpr @uub_ne_zero, mero ha), sq_nonneg (x y), sonnen (
z), nonnen (z x)
</Output>
G.2. Corrector model input-output example
### Input Example
You are helpful mathematical assistant specialized in formal theorem
+ proving using Lean4.
Your objectives:
1. Read and interpret the Lean4 theorem statement and any error messages.
2. **If previous proof attempt incorrect, analyze its exact mistakes and completely discard rewrite the proof needed.**
3. **Avoid reusing incorrect proof structures or strategies unless explicitly validated as correct.**
4. * **Address all error messages** by modifying the proof structure as needed.
5. Provide a detailed thought process in the <Thought> section, but **only
4 place the corrected Lean4 code in the <Output> section+..
6. **Ensure the new proof is logically valid and does not use 'sorry'.* :nstra are sone *xcorrect Leand theorem proof examples** for your reference. Use them as quidance when constructing the revised proof. Ensure that your final proof aligns with these examples in terms of clarity, structure, and correctness. Instruction: Natural language + theorem statement:
mathd_algebra__1
The sum the squares three consecutive positive even numbers is $12296$. Find the product of the three numbers divided by $8$. Show that it is 32736.
e Lean4 theorem statement:
.. 1eane
theorem
29

---

MA-LoT: Modc--Collaboration Lean-based Long Chain-of-Thoughe Reasoning enhances Formal Theorem Proving
(n N)
(ho Even n)
(h1 ((n:2) - 2)-2 (n:2) + ((n:2) 2)"2 = 12296)
(n - 2) n (n + 2)) / 8 = 32736 ==
0 Lean4 theorem statement and proof with explanatory comments preceding each
line code:
Response:
<Thought>
Alright, I need to prove the theorem prover_data_694 using the Lean4 code.
Here is my draft of the proof:
leann
theorem mathd_algeber 392
(n N)
(he Even n)
(hi ((n:2) - 2) + (n: + ((n:Z) 2) = 12296) ((n - 2) n * (n + 2)) / 8 32736 : by
-- Convert the equation to integers for easier manipulation norm_cast at h1 Expand and simplify the given equation ring_nf hi Solve for using numerical reasoning have h2 : = 24 by nlinarith
Substitute n = 24 into the expression and simplify
norm_num [ha]
Let me test in Lean4 Emmm, it seems the above proof is wrong.
Let me check the error messages.
OK, Here is the error messages: "*bash line 18
linarith failed to find contradiction case h1.h N
ha Even n
h Iut.aubNatNat 2 2 + (n 2) + 1(4 + n 4 2) 12296
at :n <
} False
failed
**& ""bash
line 11
unsolved goals n : N
ha Even n
hi Iub.stbNatNat 2 2 1 (n 21 <4 n 4 2) 12296
h2 24
+ False
30

---

MA-LoT: Moddl-Collaboration Lean-based Long Chain-of-Thounne Reasoning enhances Formal Theorem Proving
So, I will rethink Lean4 proof following the steps
1. Provide the natural language analysis for the theorem based on the Natural language theorem statement, Lean4 theorem statement, my previous proof and the error message.
2. Draft the Leand tactics I should use to solve the problem write the output Lean4 code.
Let analysis the wrong Lean4 solution through the error messages. ### Output Example From the error messages, it seems the following points:
"linarith failed to find a contradiction suggests that the linear arithmetic tactic was unable to derive a contradiction from the given + hypotheses, indicating that the assumptions might not lead to contradiction as expected.
case h1.h" indicates a specific case within larger context where contradiction was expected but not found, suggesting that the assumption "n < 24" might not be valid under certain conditions. uunsolved goals" means that after applying the tactics, there are still unresolved goals left, indicating that the tactics applied were - insufficient to complete the proof.
From these error messages, realize that my previous approach might not have handled the specifics of the problem correctly. Therefore, need revise my proof strategy.
First, I will analyze the natural language theorem statement and the provided Lean4 theorem statement to understand the problem fully.
The problem involves three consecutive even numbers whose squares sum to + 12296. The goal is to find the product of these three numbers divided by and show that it equals 32736.
Given that the numbers are consecutive even numbers, can denote the middle number 'n'. Then, the three consecutive even numbers be represented as "n-2", 'n', and "nt2".
The sum of their squares is given by:
((n - 2) + (n + ((n + 2) = 12296
Expanding these squares, we get:
(n - 4n 4) + n + (n + 4n + 4) 12296
Combining like terms:
32 12296
Subtracting from both sides:
3n = 12288
Dividing both sides by 3:
n 4096
Taking the square root of both sides:
31

---

MA-LoT: Modd-Coollaborttinn Lean-based Long Chain-of-Thoughl Reasoning enhances Formal Theorem Proving
64
Since are dealing with squares, take the positive root because are dealing with natural numbers. Now, the three consecut ive even numbers are:
n 2 62
n 64
2 66
The product of these numbers is:
62 * 64 66
To compute this product, can break down into smaller facters:
62 64 3968 3968 66 3968 (60 6) 3968 60 3968 6 238080 + 23808 261 868888
Now, divide this product by 8:
261888 32736
Thus, the final result matches the expected outcome. Now, I need to translate this reasoning into Lean4 code.
I will follow these steps:
1. Define the theorem with the given parameters.
2. Convert the given integer expressions to natural numbers.
3. Expand and simplify the equation using algebraic manipulation.
4. Solve for "n" using numerical methods.
5. Compute the product of the three numbers and verify that dividing by 8 gives the desired result.
I will also include necessary imports and use appropriate tactics to handle the calculations.
Now, I will proceed to write the Lean4 code following this plan. </Thought>
<Output> leaan
thoorem mathd_algebra _39
(n N)
(he Even n)
(h) ((n:Z) 2 (n:2) + ((n:Z) 2) 12296) ((n 2) n (n 2)) 8 32736 :- by Convert the equation integers for easier manipulation push_cast at h1
Expand and simplify the given equation ring_nf at hı -- Solve for n using numerical reascning have h2 : n 64 == by nlinarith
Substitute n 64 into the expression and simplify subst hg norm_num
32

---

MA-LoT: Modd--Collaboraioon Lean-based Long Chain-of- Chain-of-Thought Reasoning enhances Formal Theorem Proving
</Output>
33


Reviews:
[{"review_id": "dmWXorqyOL", "reviewer": "Reviewer_Lfxq", "summary": "This paper introduces MA-LoT, a multi-agent framework for formal theorem proving in Lean 4 combining natural language reasoning with verifier feedback. MA-LoT employs two \"agents\" (same LLM prompted in different ways): a prover that generates proofs using \"Long\" Chain-of-Thought reasoning, and a \"corrector\" that sees feedback from Lean and tries to repair proofs. The authors develop a training pipeline (LoT-TL) to gather long CoT examples from problems in existing datasets. Experiments on minif2f show MA-LoT generally outperforms other methods.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear Lfxq,\n\nWe would like to offer our sincere thanks for your constructive comments and valuable suggestions, which have helped make our paper more coherent.\n\nBecause formal theorem proving is a fast-evolving field, we would like to share with you the latest results on the MiniF2F-Test dataset for our model using a new base model named **Goedel-Prover**.\n|Method|Budget|MiniF2F-Test|\n|-|-|-|\n|Goedel-Prover-SFT|pass@32| 55.33%|\n|MA-LoT (Goedel)|16+8×2|**61.07%**|\n\nThe result under pass@32 demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.\n\nBelow are our responses to your comments:\n1. **Difference between Long CoT and normal CoT:** We have included a comparison between Long CoT and normal CoT in Appendix A.5. Generally speaking, the key difference lies in the *multi-round rethinking* capability of Long CoT, which naturally fits the context of formal theorem proving. In practice, Long CoT typically involves several rounds of natural language reasoning before producing the final output, leading to more thoroughly-thought results. In some cases, the LLM even analyzes tactics in detail before generating code under Long CoT.\n2. **Concerns about multi-agent setup:** We understand the reviewer may have seen related work that uses error messages for proof correction. However, we would like to clarify our motivation for the multi-agent setup. Our goal is to **separate cognitive tasks**: high-level proof planning is handled by the prover agent, while fine-grained error correction is handled by the corrector agent.\n\n    Our work differs from Baldur in that we incorporate natural language reasoning and multi-round thinking in Long CoT. If necessary, we are happy to tone down the “first multi-agent” claim, restrict it to the Lean4 context, rename it as “prover-corrector collaboration”, or any other suggestions regarding the naming.\n\n    Additionally, we emphasize the benefit of separating the prover and corrector agents. We designed an experiment where the prover agent attempts to correct errors using draft code and error messages as inline comments. The results are as follows, from the results, we can see that the additional corrector agent is vital for better performance.\n    |Methods|Prover|Round 1|Round 2|\n    |-|-|-|-|\n    |Prover-correction |54.92%|56.15%|57.38%|\n    |MA-LoT|54.92%|59.43%|61.07%|\n3. **Qualitative study not supported:** We do provide concrete support for the qualitative claims in the paper’s case study. To further address your concern, we have added more examples in the anonymous Git https://anonymous.4open.science/r/MA-LoT_Rebuttal_repo-516F\n4. **Additional benchmarks beyond MiniF2F:** We conducted experiments on the ProofNet-Test using the Goedel-Prover. The relative improvement of 27.33%, detailed results are shown below:\n    ||Budget|ProofNet-Test|\n    |-|-|-|\n    |**Goedel-Prover**|Pass@32|12.15%|\n    |**MA-LoT (Goedel)**|16+16|**15.47%**|\n5. **GPT-4 may be an old baseline:** We have updated our baselines for both closed-source and open-source models, now including DeepSeek-V3 and R1-Distilled-Qwen-7B. The MiniF2F-Test results are as follows, showing that MA-LoT still outperforms all the methods:\n    ||**Budget**|**MiniF2F-Test**|\n    |-|-|-|\n    |DeepSeek-V3|pass@32|33.61%|\n    |R1-Distilled-7B|pass@32|51.23|\n    | MA-LoT (Goedel)|16+2×8|**61.07%**|\n6. **Computation budget for Long CoT:** In our paper, we control the number of proofs written by the LLMs rather than the number of tokens generated, as Lean-STaR also includes natural language analysis but does not use tokens as a comparison metric.\n\n    However, we consider your review meaningful so we conduct additional experiments based on aligned GPU times. Our method consumes approximately **1.7× more GPU-hours** than traditional CoT. For fairness, we increased the sampling budget by the same factor for both DeepSeek-Prover-v1.5-RL and Goedel-Prover, and compared them with the MA-LoT framework. As shown below, even with increased computational budget, MA-LoT still outperforms the baselines, indicating a more efficient use of resources:\n    | |Budget|MiniF2F-Test|\n    |-|-|-|\n    |DS-Prover-v1.5-RL |pass@217| 52.87%|\n    |MA-LoT (DS)| 64+32×2|54.51%|\n    |Goedel-Prover |pass@53|58.20%|\n    |MA-LoT (Goedel) |16+2×8|**61.07%**|\n\n    Qualitatively, we have observed some theorems that cannot be proved using even high-budget base models; details are demonstrated in the git repo provided above.\n7. **Corrector like tree-search:** Our statement was meant as a **conceptual analogy**, not a literal claim. We will revise or remove it in the next version to avoid confusion and improve clarity.\n8. **Typos:** Thank you for pointing these out. We will correct them and fix all other typos in the next version.\n\nWe hope this rebuttal addresses your concerns, and we are deeply grateful for your insightful suggestions, which have helped improve the clarity of our paper.\n\nBest,\n\n9122 Author team", "claims_and_evidence": "There are some vague claims that I feel the authors could clarify either what exactly they mean, or simply rephrase to remove them.\n\n- \"Long CoT\": what exactly does \"Long CoT\" mean in comparison to plain old \"CoT\"? I know there is some intuition of what this means by looking at the examples from OpenAI o1 that were released in OpenAI's blog post. The paper here ablates Long CoT by switching CoT entirely. Since \"Long CoT\" is even in the title, and the motivation mentions it, I think it's important to either make this more precise or to simply call this chain-of-thought. L197, for instance, claims that the prompt specifically turns on \"Long CoT\", but I don't think the examples in the Appendix are particularly \"Long\", or that this wouldn't happen with more standard CoT prompting. One option here could be to show that, during training, the content of the <Thought> part of the output is indeed getting steadily longer.\n- The claim to be the first multi-agent setup for theorem proving is either too specific (if you just mean \"for Lean 4\"), or innacurate, since Baldur [1] showed a very similar setup a few years ago (but in Isabelle/HOL).\n- Some qualitative claims about how the proofs look (\"insightful\", \"coherent\", etc) are not evaluated in any systematic way, just mentioned in the text.\n\n[1] FIRST, Emily et al. Baldur: Whole-proof generation and repair with large language models. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 2023. p. 1229-1241.", "methods_and_evaluation_criteria": "The authors only evaluate on minif2f. While it is still a challenging benchmark, it's unclear if the resulting model performs better in other distributions of theorems, like in the mathlib splits in LeanDojo, or on Lean Workbook itself.\n\nThe claim to outperform GPT-4, but comparing to GPT-4-Turbo, is also perhaps unwarranted: this is a relatively old model by now, and trained much before the base model the authors used (DeepSeek-Prover) was trained.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "The minif2f experiment seems mostly standard. It's hard to know if the compute budget is fairly matched, since I think the approach proposed here likely generates a lot more tokens per call (the authors match the number of calls, pass@128 vs 2 x 64). This should be discussed.", "relation_to_broader_scientific_literature": "The paper tackles minif2f, which is still a challenging benchmark. The idea to have \"two agents\" is essentially the framework in Baldur, of doing proof repair besides proof generation (modulo details and formal language).", "essential_references_not_discussed": "Baldur (FSE '23), mentioned several times above.", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "* [3.2] \"for training for training\" (repeated)\n* Table 2: column name should not be \"Method\"\n* Table 3: witch-off -> switch off?", "questions_for_authors": "1. Have you measured the actual token generation differences between MA-LoT and baselines? Since each of your calls is likely to be much more expensive, tokens generated would likely be a fairer metric to match compute budgets. As it stands, it's unclear whether the gap between LoT and MA-LoT will remain, for instance.\n2. One feature of \"Long CoT\" in o1/s1/r1 seems to be that increased thinking time improves performance. Is that also true for MA-LoT? This could perhaps help you characterize your approach as \"Long CoT\". Otherwise, it doesn't look different from standard CoT, even though \"Long\" was emphasized several times.\n3. \"The corrector agent functions like the tree-search method.\" -> in what sense? This does not read like tree search.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "UgB0ktzBop", "reviewer": "Reviewer_bbL4", "summary": "This paper introduces MA-LoT, a multi-agent framework for theorem proving in Lean 4, integrating natural language (NL) reasoning with formal language (FL) verification via Long Chain-of-Thought (Long CoT). Using a novel LoT-Transfer Learning pipeline, MA-LoT enhances proof coherence and depth, outperforming GPT-4 (22.95%), single-agent tree search (49.18%), and whole-proof generation (48.30%) on the Lean4 MiniF2F-Test dataset, achieving 54.92% accuracy. Results highlight the potential of structured NL-FL reasoning for more effective formal proof generation.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear Reviewer bbL4\n\nThank you so much for your valuable comments on our paper and your appreciation of our contribution to both dataset construction and training methodology. Your encouragement truly motivates us to continue pursuing research in this field.\n\nBecause formal theorem proving is a fast-evolving field, we would like to share with you the latest results on the MiniF2F-Test dataset for our model using a new base model named **Goedel-Prover.**\n\n| Method | Budget | MiniF2F-Test |\n| --- | --- | --- |\n| Goedel-Prover-SFT | pass@32 | 55.33% |\n| MA-LoT (Goedel) | 16+8×2 | **61.07%** |\n\nThe result under pass@32 demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.\n\nTo better address your concerns, we have summarized your key questions and provided our responses below:\n\n1. **The necessity of multi-agent setup:** We understand your concern regarding the multi-agent setup. We acknowledge that our approach differs from traditional graph-based multi-agent systems that involve complex interaction between many agents. Instead, our setup sequentially applies two agents.\n    \n    The motivation behind this design is to **separate cognitive tasks**: high-level proof planning is handled by the **prover agent**, and fine-grained error correction is handled by the **corrector agent**. Our focus lies in the division of labor via the multi-agent framework, rather than building a complex interaction graph across multiple LLMs.\n    \n    To further address your concern, we conducted an experiment using a **single prover agent** to sequentially perform both whole-proof writing and error correction. In this setup, the LoT-Solver model based on the Goedel-Prover was prompted to act solely as a prover, and the error correction was done by inserting the draft code and error messages as comments in the theorem statement. The results are as follows:\n    \n    | Methods | Prover | Round 1 | Round 2 |\n    | --- | --- | --- | --- |\n    | Prover-correction | 54.92% | 56.15% | 57.38% |\n    | MA-LoT | 54.92% | 59.43% | 61.07% |\n    \n    We find that using a single prover agent for correction yields suboptimal results. The model often repeats the original proof without deeply analyzing the error, whereas the corrector agent’s **Long CoT thinking** encourages more effective debugging and correction.\n    \n2. **Advertis**e**ment of the multi-agent:** We greatly appreciate your suggestion regarding the potential over-emphasis on the multi-agent setup. While we do believe that separating the prover and corrector roles is important, we are happy to **reframe the terminology** in a future version of the paper. If necessary, we will tone down the “first multi-agent” claim or rename it as **“prover-corrector collaboration”**. Additionally, we are also open to other suggestions regarding the naming and paper writing.\n3. **Computational budget concern:** You raised an important point about whether improved results could be achieved with a larger sampling budget for DeepSeek-Prover-v1.5 and InternLM-Step-Prover. We would like to clarify that, unlike these works (and Goedel-Prover), our study focuses on **methodology**—offering a general framework that can be applied to **any base model**.\n    \n    Our experiments demonstrate that applying MA-LoT to multiple base models results in significant performance improvements. We also plan to **open-source** the dataset and training code in the camera-ready version.\n    \n    Given the methodological focus and computational cost constraints, we chose not to perform extremely large-scale experiments (e.g., pass@25,600) in this version. However, we are happy to include such experiments in a future version if the reviewer deems them necessary.\n    \n4. **Long CoT is not significant enough:** Thank you for recognizing our **Long CoT training and inference framework**. We would like to clarify that our work is not simply about applying Long CoT to formal theorem proving. Instead, our motivation lies in using **formal guidance** as the backbone of Long CoT to support more comprehensive reasoning.\n    \n    The novelty of our approach is in the deep integration of natural language (NL) reasoning and formal language (FL) feedback, where formal language acts as a hidden regularizer to guide the model’s behavior. Therefore, the significance of Long CoT is not only in the method itself but also in the conceptual framework it introduces. Reviewer tBG8 also considers our contribution is suitable for ICML. We will add this clarification in the next version of the paper.\n    \n5. **Typo problem:** Yes, the “54.92%” figure in the abstract and conclusion is a typo. We will update it to reflect the correct result based on the Goedel-Prover base model in the next version.\n\nWe are more than grateful for the reviewer’s appreciation of our Long CoT training inference framework and hope that our rebuttal has settled your concerns.\n\nSincerely,\n\n9122 Author team", "claims_and_evidence": "While the paper claims to introduce “the first multi-agent framework for Lean 4 theorem proving that balances NL reasoning and FL verification in Long CoT”, the necessity of a multi-agent setup is not convincingly justified. The interactions between agents could potentially be replicated by a single agent operating sequentially, generating a proof first and then refining it according to the feedback from Lean in an iterative manner. \n\nThe paper does not provide compelling evidence that a multi-agent approach yields inherent advantages over a well-structured single-agent framework following the same reasoning pipeline. Without empirical ablations comparing multi-agent interaction to sequential single-agent processing, the claim that multi-agent coordination is essential remains unsubstantiated. \n\nHowever, the Long CoT aspect of the claim is well-supported, as the paper presents new training data and field-specific alignment strategies that demonstrate its impact on proof generation quality.", "methods_and_evaluation_criteria": "The proposed methods make sense for formal theorem proving. My impression is that the Long CoT pipeline including the field-specific alignment strategy is perhaps what contributes to the improved performance most.", "theoretical_claims": "The paper is mostly empirical.", "experimental_designs_or_analyses": "The experimental designs and analyses look reasonable. Limiting other approaches sample budget is acceptable for fair comparison. It is known, however, that some of the methods (e.g., InternLM2.5-StepProver (7B) and DeepSeek-Prover-V1.5-RL (7B) ) in table 1 surpass the best performance of the submission when given more sample budget.", "relation_to_broader_scientific_literature": "The long CoT pipeline can potentially be used to generate training data suitable for theorem provers other than Lean.", "essential_references_not_discussed": "The references look reasonable.", "other_strengths_and_weaknesses": "My major complaint is the advertisement of the approach being multi-agent. The framework can in principle be done by a single agent operating sequentially. Moreover, Table 1 suggests that the major performance boost comes from the long CoT, and the benefits from correction based on Lean’s feedback seem relatively small.\n\nFactoring out the contribution of the so-claimed “multi-agent”, the long CoT pipeline itself is not particularly significant for a research paper. I do appreciate the amount of work put into compiling / enhancing a new dataset for Lean, though.", "other_comments_or_suggestions": "In the abstract and conclusion the authors report 54.92% accuracy, but throughout the entire experiment section I only see 54.51%. A typo?", "questions_for_authors": "Nothing in particular.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "nBDyWgz9O0", "reviewer": "Reviewer_tVG8", "summary": "This paper proposes the MA-LoT framework, which incorporates a long CoT with an iterative refinement approach to improve formal theorem-proving ability. The model first makes an attempt using NL planning followed by FL proof. If the attempt is incorrect, the initial prompt is combined with the error message to generate a second attempt. To enable this capability, the model is first fine-tuned on NL long CoT data from the OpenO1-SFT-Pro dataset. Then, it is trained on FL proof data with NL annotations. To collect FL-NL aligned data, this paper also introduces a pipeline for dataset creation.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear Reviewer tVG8\n\nThank you so much for your appreciation of our work. We are sincerely grateful that you consider it suitable for ICML.\n\nWith our deepest thanks for your constructive comments, we would like to share the latest results on the MiniF2F-Test dataset using a new base model named **Goedel-Prover**:\n|Method|Budget|MiniF2F-Test|\n|-|-|-|\n|Goedel-Prover-SFT|pass@32|55.33%|\n|MA-LoT (Goedel)|16+8×2|**61.07%**|\n\nThe result under the pass@32 metric demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.\n\nTo address your concerns more clearly, we summarize your points and provide our responses below:\n\n1. **Multi-agent setup problem:** We are truly thankful for your detailed understanding of our work and related efforts in the field. You raised an important point that some prior works may have used error messages in conjunction with tree search. However, to our knowledge, neither DeepSeek-Prover-v1.5 nor Lean-STaR uses error messages during the tree search process. Our work, as far as we know, is the first in the context of Lean4 theorem proving to explicitly incorporate error messages within a multi-agent Long CoT framework. We will clarify this point in the next version.\n\n    The motivation for our multi-agent setup is to **separate cognitive tasks**—with the prover agent handling high-level proof planning and the corrector agent focusing on fine-grained error correction. This is more effective than simply using a prover agent for tree search without such separation.\n\n    To validate this, we conducted an experiment where the prover agent was used to perform both full-proof generation and error correction. This was done by including the draft code and error message as comments in the theorem statement. The results using Goedel-Prover on the MiniF2F-Test are as follows:\n    |Methods|Prover|Round 1|Round 2|\n    |-|-|-|-|\n    |Prover-correction|54.92%|56.15%|57.38%|\n    |MA-LoT|54.92%|59.43%|61.07%|\n\n    As shown, using the prover for error correction results in suboptimal performance. However, we appreciate your suggestion and are happy to tone down the \"first multi-agent\" claim. We are also open to renaming it as **“Prover-Corrector Collaboration”** or adopting any alternative phrasing that better conveys the contribution without overstating the novelty.\n\n2. **Concerns about SOTA performance:** We are grateful for your thoughtful critique and would like to break down our response into three parts:\n    1. Differences in measured baselines vs. reported values: We are aware that our measured baseline results differ from those reported in the DeepSeek-Prover paper. This discrepancy likely stems from our machine being unable to install vllm. A similar degradation was also observed in the Goedel-Prover baseline and other experiments. We will clarify this technical limitation in the paper.\n    2. Suboptimal whole-proof accuracy: We appreciate your effort to compare the model capability of LoT-Solver to other base models. While our results may be degraded due to infrastructure constraints, our focus is on the overall framework rather than standalone model performance. Even with baseline degradation, the MA-LoT framework still achieves a 5.64% relative improvement over DeepSeek-Prover-v1.5 and 6.02% over Goedel-Prover. Additionally, we observed some theorems that cannot be solved even with a large computational budget (e.g., pass@256). We include a detailed example in https://anonymous.4open.science/r/MA-LoT_Rebuttal_repo-516F\n\n    3. Other works have higher accuracy under a larger computational budget: We appreciate the suggestion to explore higher performance using larger budgets (e.g., 32 × 6,400 search). However, the main contribution of our work lies in the methodology. Therefore, we only conducted experiments under a smaller budget. However, we are more than happy to include large-budget experiments in a future version if you think it necessary.\n3. **Computational efficiency for the Long CoT method:** We appreciate your suggestion that Long CoT may consume more computational resources under the same pass rate. To address this, we evaluated GPU usage and compared the efficiency of MA-LoT against baselines.\n\n    We found that MA-LoT consumes ~1.7× more GPU hours. For fairness, we scaled the sampling budget for DS-Prover-v1.5-RL and Goedel-Prover accordingly and compared them with MA-LoT. As shown below, MA-LoT still outperforms the baselines, demonstrating a more efficient use of the computational budget:\n    ||Budget|MiniF2F-Test|\n    |-|-|-|\n    |DS-Prover-v1.5-RL|pass@217|52.87%|\n    |MA-LoT (DS)|64+32×2|54.51%|\n    |Goedel-Prover|pass@53|58.20%|\n    |MA-LoT (Goedel)|16+2×8|**61.07%**|\n\n4. **Title concerns:** We will use a shorter title in the next version.\n\nWe are grateful for the reviewer’s appreciation of our methodology and constructive comment, and we hope that our rebuttal has settled your concerns.\n\nSincerely,\n\n9122 Author team", "claims_and_evidence": "1. The model claims to be the first to use a multi-agent framework for Lean4 theorem proving. However, this framework essentially involves the model making an initial attempt, receiving an error message, and then generating a second attempt based on the first attempt and the error message. This process is repeated iteratively. A similar approach has already been explored. For example, DeepSeek-Prover-v1.5 has utilized error messages in a tree-based search setting. Additionally, many other papers, such as “Proof Automation with Large Language Models” and “An In-Context Learning Agent for Formal Theorem Proving”, have investigated similar ideas.\n2. DeepSeek-Prover-v1.5-RL achieved an accuracy of 51.6% ± 0.5% on the miniF2F-test for 128@pass whole-proof generation in the original paper, whereas this paper reports the accuracy as 48.36%. The whole-proof accuracy of LoT is 52.05%, which only marginally surpasses the original DeepSeek-Prover-v1.5-RL results (within one standard deviation). For tree search-based methods, DeepSeek-Prover-v1.5-RL achieves an accuracy as high as 63.5%, which exceeds MA-LoT’s performance. These experimental results suggest that MA-LoT does not outperform the SOTA methods.", "methods_and_evaluation_criteria": "The metric and evaluation criteria are fine.", "theoretical_claims": "N/A.", "experimental_designs_or_analyses": "The overall experimental design is good. However, it would be beneficial to include computational efficiency in the evaluation; otherwise, the tree-search-based DeepSeek-Prover-v1.5-RL may achieve higher accuracy. Additionally, the high computational overhead is a major drawback of long CoT reasoning.", "relation_to_broader_scientific_literature": "This paper extends the long CoT method to the formal theorem proving.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "1. I will currently rate the paper as a 2, but I am open to increasing the score if my concerns are properly addressed. Overall, I believe the paper is suitable for ICML; however, the unnecessary emphasis on the multi-agent framework (is it truly essential to make it the core of the story?) and the omission of some SOTA results raise concerns. In my opinion, the main contribution is extending the long CoT method to the formal theorem-proving method.\n2. Please remember to include a short title.", "questions_for_authors": "N/A.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper introduces the MA-LoT framework, a multi-agent system designed to enhance formal theorem proving in Lean4 by integrating natural language reasoning with formal language verification through a Long Chain-of-Thought (Long CoT) approach. The authors claim that this framework is the first of its kind for Lean4 theorem proving, achieving significant improvements over existing methods.

(+) The framework demonstrates a notable improvement in accuracy on the Lean4 MiniF2F-Test dataset, outperforming several baseline models, including GPT-4 and other single-agent methods.  
(+) The authors provide extensive experimental results, including comparisons with various baselines and ablation studies to highlight the effectiveness of their approach.  
(-) The necessity and novelty of the multi-agent setup were questioned by reviewers. The interactions between agents could potentially be replicated by a single agent operating sequentially, and similar approaches have been explored in other contexts.  
(-) The high computational overhead of the Long CoT reasoning was noted as a drawback, and the evaluation did not initially include a suitable metric for computational efficiency.  

The authors actively engaged with reviewers during the rebuttal phase, addressing concerns and providing additional experiments and clarifications.

The paper presents a promising approach to formal theorem proving with a well-structured framework and significant empirical results. While there are concerns about the novelty of the multi-agent setup and baseline comparisons, the authors have addressed these issues satisfactorily in their rebuttal. Assuming the promised revisions are made, I recommend the paper for acceptance.
Decision: Accept (poster)