PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2503.03205v3cs.CLcs.AI

TL;DR

Single-model Lean proving struggles to balance natural-language reasoning with formal-verifier feedback. MA-LoT separates proof planning from verifier-guided correction and reports 61.07% accuracy on MiniF2F-Test, above cited whole-proof and tree-search baselines.

  • Problem

    Single-model approaches struggle to balance natural-language reasoning with formal verifiability, while ambiguity in natural language complicates checking intermediate mathematical steps.

    Source: §1 · pp. 1, 3

  • Method

    MA-LoT coordinates a prover for high-level proof planning and writing with a corrector that refines proofs using Lean4 feedback, supported by LoT-TL transfer learning without specifically annotated formal Long CoT data.

    Source: §1 · p. 3, §2.2 · p. 4

  • Results

    61.07% accuracy on MiniF2F-Test; MA-LoT surpasses Godel-Prover (55.33%) and InternLM-Step-Prover (50.70%).

    Source: §1 · p. 3, §3.3 · p. 7

  • Takeaways & Limitations

    The authors conclude that combining Long CoT reasoning, formal verification, and model collaboration enhances discovery of non-trivial, in-depth proofs.

    Source: §3.3 · p. 8

    Without vLLM, reported DeepSeek-Prover and Goedel-Prover results differ from the originals with a slight capability drop; vLLM could not fit their machine, raising evaluation cost.

    Source: §3.2 · p. 6

Abstract

from arXiv · show

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.

1. Introduction

Existing single-model approaches struggle to balance high-level natural-language planning with formal verification feedback. MA-LoT combines a prover and corrector through Long CoT, supported by a training pipeline that needs no specifically annotated formal data.

1. Introduction

  • Tree-search methods verify each generated step but become computationally expensive as proofs grow and lack high-level planning for structured proofs.Whole-proof generation uses natural-language reasoning and high-level planning with predictable computation costs, but lacks verifier feedback and post-hoc error analysis.Source: §1 · pp. 2–3
  • MA-LoT separates high-level proof planning and writing from fine-grained correction using Lean4 verifier feedback, with both roles supported by Lean4-specific Long CoT.The prover drafts a proof; the corrector interprets verifier feedback and refines it.Source: §1 · p. 3
  • LoT-TL transfers across general natural-language Long CoT, theorem-proving SFT, and Lean4 feedback pairs to develop formal Long CoT without specifically annotated formal data.The pipeline aims to preserve natural-language reasoning and planning while building awareness of formal proof states and tactics.Source: §1 · p. 3
  • 61.07% accuracy on MiniF2F-Test under similar sampling budgets exceeds whole-proof generation Godel-Prover (55.33%) and tree-search InternLM-Step-Prover (50.70%).The framework also proves some advanced IMO and AIME problems in MiniF2F that existing models struggle with.Source: §1 · p. 3
  • The authors identify potential beyond Lean4 theorem proving for integrating formal verification with Long CoT generation.They describe iterative planning and error analysis on formal executors as a route toward structured, reflective, and adaptable text generation.Source: §1 · p. 3

2. Methodology

The methodology develops Lean4-specific Long CoT through LoT-TL, then uses the resulting LoT-Solver as both a whole-proof prover and a verifier-feedback corrector. It covers preliminary approaches, training data and stages, and the collaborative proof-writing process.

2.1. Preliminaries

  • The approach combines tree-search and whole-proof generation strengths by coordinating natural-language reasoning and formal-language verification through Long CoT.The methodology’s core aim is deep integration of natural-language and formal-language reasoning under Lean4 theorem proving.Source: §2 · p. 3, §2.1 · p. 4

2.2. LoT-TL Training Pipeline

  • LoT-TL uses system prompts to control training and inference across general natural-language Long CoT, field-specific SFT, and correction data, without annotated Long CoT data.The pipeline comprises collecting field-specific SFT data, training general natural-language Long CoT, and transfer learning on SFT and correction data.Source: §2.2 · p. 4

2.2.1. OBTAIN SFT DATA

  • LoT-ProveData contains 54,465 records of Lean4 statements, verified proofs with natural-language explanations, and natural-language statements; LoT-CorrectionData contains 64,912 correct-incorrect proof pairs with error messages.The correction records are used to train error analysis and correction; the proof dataset is assembled from existing proof sources with generated natural-language explanations and statements.Source: §2.2.1 · p. 4

2.2.2. NL LONG COT TRAINING

  • The second training stage uses standard next-token SFT on 126k OpenO1-SFT-Pro math and science examples to train natural-language Long CoT before final answers.The model gains natural-language Long CoT, but when applied to Lean4 it tends to output natural-language solutions rather than Lean4 code, motivating further alignment.Source: §2.2.2 · pp. 4–5

2.2.3. FIELD-SPECIFIC ALIGNMENT

  • Field-specific alignment trains first on LoT-ProveData, then LoT-CorrectionData, using a placeholder Long CoT structure and prompts that control its use at inference.The authors report that Lean4 proof and error-analysis Long CoT abilities emerge when Long CoT is turned on at inference; LoT-Solver is trained from an expert Lean4 prover.Source: §2.2.3 · p. 5

2.3. Model-Collaboration Lean4 Proof Writing

  • The model-collaboration framework uses LoT-Solver as the base for both roles: a prover drafts a complete proof and a corrector analyzes and fixes it from Lean verifier feedback.This arrangement combines whole-proof generation and tree-search methods under the Lean-based Long CoT paradigm.Source: §2.3 · p. 5

2.3.1. PROVER MODEL

  • The prover generates an initial whole-proof Lean4 draft, uses Long CoT for a high-level plan, and submits the proof to Lean4 for verification.An incorrect proof is passed to the corrector for refinement.Source: §2.3.1 · p. 5

2.3.2. CORRECTOR MODEL

  • The corrector analyzes an incorrect proof alongside Lean verifier feedback in Long CoT, rethinks the strategy, and produces a revised proof; correction can repeat until success or the retry limit.The authors describe this feedback-based process as enabling deeper reflection and exploration of alternative proof strategies while maintaining computational efficiency.Source: §2.3.2 · pp. 5–6

3. Experiments

MA-LoT is evaluated on MiniF2F-Lean4 through benchmark comparisons, correction and efficiency studies, training ablations, and qualitative case studies. The experiments report stronger results with model collaboration and Long CoT, while examining the contribution and cost of these components.

3.1.1. DATASET AND TASK

  • The test and validation sets each contain 244 Lean4 statements, ranging from high-school competition questions to undergraduate-level theorem proofs.The task is to generate Lean4 proofs from formal statements and natural-language descriptions; imports are manually configured to reduce computational overhead.Source: §3.1.1 · p. 6

3.1.2. BASELINES

  • The evaluation covers tree-search and whole-proof baselines, with whole-proof sampling budgets generally set to pass@128, except Godel-Prover at pass@32.The authors align tree-search costs as closely as possible with whole-proof generation.Source: §3.1.2 · p. 6

3.3. Results

  • 61.07% accuracy on MiniF2F-Test; MA-LoT surpasses state-of-the-art tree-search and whole-proof baselines, while LoT-Solver whole-proof reaches 57.79%.The main table reports results for the whole pipeline and whole-proof generation.Source: Table 1 · p. 7, §3.3 · p. 7

3.4. Corrector study

  • During the first three correction rounds, the corrector fixes an average of 11.55% of theorems the prover cannot answer, often on difficult IMO, AIME, and high-level MATH problems.Using the prover itself as corrector instead causes a performance drop in both rounds, as it tends to repeat the incorrect proof.Source: Table 2 · p. 7, §3.4 · p. 8

3.5. Long CoT Efficiency Study

  • MA-LoT generates 33% more tokens and costs 70% more GPU hours, yet outperforms a base model with 1.7 times the sampling budget by 4.93%.The comparison adjusts the base model's sample budget to account for MA-LoT's additional GPU hours.Source: Table 4 · p. 7, §3.5 · p. 8

3.6.1. EFFECT OF TRAINING STAGES

  • NL Long CoT training alone yields minimal improvement; adding theorem-proving SFT via LoT-TL markedly improves performance, and correction-data training further enhances it.The correction-data improvement is attributed as likely arising from self-analysis capabilities in Lean4 code.Source: Table 3 · p. 7, §3.6.1 · p. 8, §3.6 · p. 8

3.6.2. SWITCH-OFF LONG COT

  • Switching off Long CoT drops performance from 51.64% to 49.18%; direct RL-data fine-tuning without it reaches 48.36%, below LoT-Solver’s 51.64%.Without Long CoT, the model lacks an explicit high-level plan and misses some induction problems.Source: §3.6.2 · pp. 8–9, §3.6.3 · p. 9

3.7. Case Study

  • Case studies show the prover planning advanced MATH proofs and the corrector using Lean-executor feedback to formulate a correct proof for an IMO-level problem.The authors describe these examples as qualitative evidence of collaboration and emergent formal reasoning in Long CoT.Source: §3.7 · p. 9

4. Related Work

Prior Lean theorem-proving work uses tree search, whole-proof generation, or attempts to combine models, with different trade-offs in natural-language planning and formal feedback. Broader LLM-collaboration methods separate cognition tasks, but formal-reasoning systems still face a gap in high-level analysis and Long CoT.

4.1. Lean4 Theorem Proving using LLMs

  • Tree-search approaches can incur exponentially increasing computation and miss high-level natural-language planning, while whole-proof generation lacks thorough use of Lean verification feedback.Earlier combined-model approaches also underperformed because they lacked thorough natural-language reasoning and multi-round Long CoT.Source: §4.1 · p. 9
  • Prior theorem-proving approaches include tree search and whole-proof generation, with early model-combination work also explored.The section describes tree search as using an LLM to generate proof steps and whole-proof generation as producing an entire proof without executor interaction.Source: §4.1 · p. 9

4.2. LLM Collaboration

  • Tree-search methods iteratively query an executor for feedback, but the natural-language/formal-language gap limits their ability to analyze problems at a high level and respond structurally.The cited methods include ReProver, Lean-Star, and InternLM-Step-Prover.Source: §4.2 · p. 9

5. Conclusion

MA-LoT coordinates a prover and corrector through Lean-based Long CoT, while LoT-TL trains this capability without specially annotated Lean Long CoT data. On MiniF2F, MA-LoT reports 61.07% accuracy and surpasses the baselines; the authors point to wider uses for transfer learning and formal verification.

5. Conclusion

  • 61.07% accuracy on MiniF2F is reported for MA-LoT, surpassing all baselines, including tree-search and whole-proof-generation methods.The conclusion highlights combining formal verification with structured, iterative Long CoT reasoning.Source: §5 · p. 9
  • MA-LoT coordinates prover and corrector models through Lean-based Long CoT, separating high-level proof planning from fine-grained correction.The conclusion describes this as addressing single-model approaches that miss either natural-language reasoning capability or formal feedback integration.Source: §5 · p. 9
  • LoT-TL enables domain-specific Long CoT reasoning without specially annotated Lean Long CoT data, and the authors suggest it may extend to specialized domains beyond theorem proving.The conclusion also suggests broader applications of model-collaboration Long CoT with formal verification for structured reasoning.Source: §5 · p. 9

Impact statement

The impact statement identifies education as the main potential social-impact area and notes that ethical concerns are too early for specific discussion. The term chart defines the paper's methods, model, and training datasets.

Impact statement

  • The stated potential social impact is in education, where more capable formal theorem provers may make it harder to distinguish model-generated results from student writing.The authors say specific ethical-concern discussions are too early at this stage.Source: Impact statement · p. 10

A. Term chart

  • Long CoT denotes extended, multi-step reasoning before proof generation, reflection, and iterative refinement using Lean4 feedback..Source: A. Term chart · p. 13
  • MA-LoT is the proposed model-collaboration framework, and LoT-TL is its transfer-learning pipeline for Lean4 Long CoT capability without specially annotated data.LoT-Solver is trained through LoT-TL and serves as both prover and corrector.Source: A. Term chart · p. 13
  • LoT-PD contains verified Lean4 proofs with natural-language statements and proofs to provide prover capability, while LoT-CD pairs incorrect proofs and error messages with correct proofs and annotations for refinement..Source: A. Term chart · p. 13

B. Examples for tree-search and whole-proof generation

The examples contrast producing an entire Lean proof with generating a proof incrementally through tree-search steps. One whole-proof example uses an algebraic inequality, while the tree-search example presents a natural-number theorem and an induction step.

B. Examples for tree-search and whole-proof generation

C. Scaling Law Study

The scaling study finds accuracy rises nearly linearly with log-scaled training steps on MiniF2F-Test. Its results suggest performance may benefit from larger-scale training and additional Lean4 data.

C. Scaling Law Study

  • The study evaluates four training-step counts—125, 250, 1250, and 2500—with batch size fixed at 4.Accuracy is evaluated on MiniF2F-Test using Long CoT.Source: C. Scaling Law Study · p. 13
  • R2=0.9664 for the linear fit between log-scaled training steps and MiniF2F-Test accuracy, indicating near-linear improvement as training steps increase.The authors suggest the approach benefits from larger-scale training and that expanded resources could support annotation of additional Lean4 data.Source: C. Scaling Law Study · pp. 13–14, Figure 3 · p. 14

D. ProofNet result

The ProofNet comparison reports higher accuracy for MA-LoT than the original Goedel-Prover, though the two figures use different evaluation metrics. Case studies describe a prover that plans proofs in natural language and a corrector that uses Lean feedback to produce correct proofs.

D. ProofNet result

  • 15.47% accuracy for MA-LoT(Goedel) under 16+16, versus 12.15% for the original Goedel-Prover under pass@32 on ProofNet.The authors call this a small-scale comparison and note that Goedel-Prover does not fit ProofNet well, as reported by Lin et al. (2025).Source: D. ProofNet result · p. 14

E. Case studies

  • The prover writes a more coherent, structured proof by making a high-level natural-language plan, while the corrector analyzes unsolved goals and writes a correct proof.The authors attribute these case-study behaviors to their training procedure.Source: E. Case studies · p. 14

E.1. Prover analysis

The prover example shows Long CoT organizing a theorem solution as natural-language reasoning followed by a high-level plan and Lean4 code. The illustrated modular-arithmetic argument concludes that n % 4 = 3 from n % 8 = 7.

E.1. Prover analysis

  • The prover uses a high-level proof plan in Long CoT, then executes its details in Lean4 code.The provided header asks for natural-language analysis, draft tactics, and output Lean4 code.Source: §E.1 · p. 15
  • From n % 8 = 7, the example uses that 4 divides 8 to derive n % 4 = 3.The displayed reasoning reduces the remainder to 7 % 4.Source: §E.1 · p. 15

E.2. Corrector analysis

The corrector example illustrates Long CoT error analysis: after an initial proof leaves the goal unsolved, the model rethinks its approach and produces a successful proof for an IMO-level problem.

E.2. Corrector analysis

  • The IMO-level correction example analyzes the error message, makes a proof plan, and then writes a correct proof.The paper presents this sequence as an example of successful error correction.Source: §E.2 · p. 15
  • The initial proof leaves the target inequality as an unsolved goal, which the model identifies as the central issue in its subsequent analysis.The reported error message shows the remaining inequality explicitly.Source: §E.2 · pp. 16–17
  • The authors connect the example’s rethinking process in Long CoT with reaching a conclusion that requires more thorough thinking.Their corrected proof invokes non-negativity of squared differences and nonlinear arithmetic.Source: §E.2 · pp. 18, 21

E.3. Theorem only solved by MA-LoT

The section presents a theorem solved only in the MA-LoT setup and illustrates how Lean error feedback led the corrector to restructure an incorrect proof. The revised approach solves for z first, then uses it to obtain f.

E.3. Theorem only solved by MA-LoT

  • The theorem algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7 is reported as solved only in the MA-LoT setup.The authors attribute this example to the corrector's ability to rethink and restructure the proof using formal guidance.Source: §E.3 · p. 21
  • Lean reported a type mismatch and a separate ring failure in the attempted proof.The error output says a proposition `z = 7` was expected to have another type and that the ring expressions were not equal.Source: §E.3 · p. 23
  • The corrected proof derives z = 7 first, substitutes it into f = 11 - 3*z to obtain f = -10, and combines both results.This replaces the earlier separate left-and-right case structure.Source: §E.3 · pp. 24–25

F. Training examples

The training examples show how LoT-TL handles SFT and correction data, followed by prover and corrector input-output examples. Long CoT is disabled differently for the two training-data types.

F. Training examples

  • LoT-TL disables all Long CoT for SFT data, but correction data retains the error message and proof draft while disabling error-message analysis.The passage presents these as distinct training settings.Source: F. Training examples · p. 25

F.1. LoT-TL Training example for SFT data

  • The SFT example requests a Lean proof without Long CoT and shows a commented proof for an equality of identical rational expressions.The example response uses `congr 1`, simplification, and numerical normalization.Source: §F.1 · pp. 25–26

F.2. LoT-TL Training example for correction data

  • The correction example supplies Lean errors and a draft, while directing the model to use errors in Long CoT without providing natural-language error analysis.The revised output gives a tactic proof for an inequality under non-negativity and a sum-to-one condition.Source: §F.2 · pp. 26–27

G.1. Prover model input-output example

  • The prover example requests natural-language analysis, Lean4 tactic planning, and code, illustrating proofs of 0 < a, b^2 < a^2, and a^2 < 3*b^2 under the single condition x*y=z^2.Source: §G.1 · pp. 28–29

G.2. Corrector model input-output example

  • The corrector instructions require interpreting Lean errors, addressing them, and discarding or rewriting incorrect proof structure; the example includes failed linarith and unsolved goals.The instructions also say the corrected proof must not use `sorry`.Source: §G.2 · pp. 29–30

Related papers

Loading 2503.03205v3…