Pith. sign in

REVIEW 3 major objections 3 minor 2 cited by

Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning

T0 review · 3 major / 3 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that verifier-integrated long chain-of-thought lets a 7B model reach 78.2% pass@128 on MiniF2F-test, a new small-model state of the art.

desk verdict Real system-level gains and a useful engineering recipe, but the paper's central claim that RL training drives the improvement is not supported by its own ablations. read the letter →

arxiv 2507.08649 v1 pith:VKFY3A5T submitted 2025-07-11 cs.AI

Xingguang Ji , Yahui Liu , Qi Wang , Jingyuan Zhang , Yang Yue , Rui Shi , Chenxi Sun , Fuzheng Zhang
show 2 more authors
Guorui Zhou Kun Gai
This is my paper
classification cs.AI
keywords formaltheoremprovingLean4reinforcementlearningverifierfeedbackchain-of-thoughttokenmaskingself-correctionsmalllanguagemodels
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that a small 7B language model can become a much stronger formal theorem prover if it is trained to call the Lean 4 verifier inside its own reasoning trace and to revise its proof in response to the verifier's error messages. The authors post-train two existing 7B provers with a cold-start supervised stage and then a reinforcement-learning stage whose reward is verifier success or failure. On MiniF2F-test they report pass@128 of 70.4% from Kimina-Prover-Preview-Distill-7B and 78.2% from DeepSeek-Prover-V2-7B, roughly matching what the Kimina baseline needs 1024 samples to achieve. If true, this would make verifier feedback a practical substitute for much of the sample budget and brute-force search in neural theorem proving.

What carries the argument

The load-bearing mechanism is the verifier-integrated long chain-of-thought loop: the model writes Lean 4 code inside <code> delimiters, the Lean 4 verifier compiles it and returns either success or a concrete error, and the error is inserted between <interpreter> delimiters as a reflection prompt for the next round. Feedback token masking keeps the model's loss on verifier-provided tokens at zero, both in cold-start SFT and in RL, so the policy learns from its own rewritten proof tokens rather than from the verifier text; DAPO supplies a token-level policy gradient and clip-higher objective, and the reward is simply format plus compilation success or failure. This machinery turns the verifier into a state-dependent tool whose feedback is tightly coupled to logical correctness.

What would settle it

Run the trained verifier-integrated model and the vanilla RL control under the same evaluation protocol, with no second verifier pass: the paper's own Table 3 already shows the Kimina-based model at 64.7% pass@32 versus 65.5% for vanilla RL, so the policy itself, not the extra reflection, must account for the reported advantage. Alternatively, give the vanilla RL model the same verifier-reflection iterations at test time; if it matches the proposed model, the training signal is not the source of the improvement.

Watch

Extended reading notes

Core claim

In the paper's own terms, the central discovery is that a formal verifier can be used as an interactive tool inside long chain-of-thought, and that reinforcement learning over multi-turn verifier interactions teaches the model a reflection policy: generate a Lean 4 snippet, read the compilation log, rewrite the proof, and repeat until the verifier accepts. The authors formulate the objective as maximizing the probability that a proof rewritten after verifier feedback passes verification, and they report that this verifier-integrated RL outperforms vanilla RL on both base models, with the largest gain, 5.3 points at pass@32 on MiniF2F-test, coming on the weaker Kimina base. They also report that most of the gain appears in the first verifier-calling iteration, and that further iterations help only the Kimina-based model.

Load-bearing premise

The causal attribution of the reported gains to the RL training procedure presupposes that the vanilla RL baseline would not gain equally if it were allowed the same verifier reflection at evaluation time.

Editorial extensions

If this is right

  • A 7B model post-trained this way reaches 78.2% pass@128 on MiniF2F-test, and reaches the performance the Kimina baseline only attains at pass@1024.
  • Verifier-calling iterations are the main source of near-term gain: one corrective round adds 3.7 points for the Kimina-based model, while a second and third round add about 0.4 points each.
  • The method transfers beyond olympiad-style problems: ProofNet-test gains 6.4 points at pass@128 on the Kimina base, and the DeepSeek-based model solves one additional AIME 24&25 problem.
  • On an already RL-tuned model such as DeepSeek-Prover-V2-7B, the training gains are smaller, and the authors attribute the diminishing returns to a shortage of active training prompts at higher difficulty.
  • A simple success or failure reward is sufficient; fine-grained rewards derived from the proof's abstract syntax tree do not help, with tactic-count reward giving only a slight gain and automation and state-change rewards performing worse.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the main effect is inference-time reflection rather than RL-trained self-correction, then a baseline model prompted to call the verifier iteratively could capture much of the reported gain without any RL; the paper's own Table 3 makes this a live possibility for the Kimina base.
  • The same verifier-integrated loop should transfer to other interactive theorem provers and to any setting with a deterministic checker that returns structured errors, such as code execution or constraint solvers.
  • A clean testable extension would compare, at equal sampling budget and equal number of verifier calls, the fully trained policy against the cold-start SFT model used as the RL initialization; this would separate what RL adds from what the verifier loop itself provides.
  • Because the training data is filtered to problems with pass rates between 1/8 and 1/2, the method is biased toward problems the base model can almost solve; harder sets such as IMO may show smaller gains, consistent with the authors' stated limitation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper introduces Leanabell-Prover-V2, a 7B-parameter model for Lean 4 theorem proving trained with a cold-start supervised fine-tuning (SFT) stage on synthesized long chain-of-thought data, followed by DAPO reinforcement learning (RL) with feedback from the Lean 4 verifier. The authors report improvements over two base models, Kimina-Prover-Preview-Distill-7B and DeepSeek-Prover-V2-7B, on MiniF2F-test, ProofNet-test, and ProverBench, and claim that verifier-integrated RL training, rather than verifier use at inference, drives these gains.

Significance. If the causal claim were established, the result would be notable: a 7B prover reaching 78.2% pass@128 on MiniF2F-test and a training recipe that makes verifier feedback usable by small models would be of broad interest. The paper also contributes a verifier-feedback token-masking strategy and states that code and data are released, which are strengths. However, the evaluation does not isolate the RL contribution, and the paper's own ablations contradict the causal attribution to RL training.

major comments (3)
  1. [§3.1 (Tables 2 and 3)] The comparison in Table 2 between 'Vanilla RL' and 'Our RL' is not matched in evaluation protocol. Table 3 reports that Leanabell-Prover-V2-KM evaluated on its first generated <code> block without any verifier reflection ('32 (Vanilla)') scores 64.7% at pass@32, which is below the 65.5% of the vanilla RL control; the 68.4% figure used in Table 2 corresponds to row '32-1', i.e., after one verifier-calling iteration. Therefore the headline 2.9-point advantage over vanilla RL is attributable to extra inference-time reflection compute rather than to the RL training method. The same pattern holds for DeepSeek-Prover-V2-7B (75.4% without reflection vs 75.6% vanilla RL). This directly undermines the abstract's and Section 1's claim that verifier-integrated RL 'significantly enhances the model's capabilities.'
  2. [§2.2 and §3.1 (Table 2)] The proposed method prepends a cold-start SFT stage (roughly 7K samples, including Claude-3.7-Sonnet-rewritten 'incorrect-corrected' pairs) to the RL stage, but the paper never evaluates the SFT-only checkpoint or an SFT + vanilla RL control. Consequently, the gains attributed to 'Our RL' could be due to the SFT data alone, which already teaches the verifier-calling format and corrective rewriting. Without this ablation, the RL-specific contribution is not identified.
  3. [§3.1 (Table 3)] The verifier-calling ablation shows that the first reflection iteration accounts for 3.7 of the total 4.5-point improvement for the KM variant (64.7% to 68.4% out of 69.2% at three iterations). This is consistent with the hypothesis that the observed gains are an inference-time self-correction effect available to any model given verifier feedback, rather than a behavior learned through RL. The paper should test whether the vanilla RL baseline, if allowed the same verifier-calling interface at inference, exhibits similar improvements; without such a control, the RL training contribution is not supported.
minor comments (3)
  1. [§1] The sentence 'we continual to choose to posttrain existing strong prover models' should be reworded; also 'addtion' (§3.1), 'obatain' (§3.1), 'promissing' (§3.1), 'provied' (§2.3), 'bewteen' (Appendix D), and 'heve' (Appendix C) are typos.
  2. [Table 3] The label 'Vanilla' in Table 3 to denote evaluation without verifier-calling iterations is confusing because Table 2 uses 'Vanilla RL' for a training baseline; consider renaming the row to 'Iteration 0' or 'w/o verifier call.'
  3. [§3.1] The statement that pass@128 with our method reaches the baseline's pass@1024 performance ('70.4% v.s. 70.8%') should explicitly note that the comparison involves different inference budgets and additional verifier reflection rounds, so the claim of 'inference efficiency gains' is not a direct measure of wall-clock or token cost.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: benchmark numbers are direct external measurements; the verifier-refinement confound in Tables 2–3 is an attribution issue, not a constructed equivalence.

full rationale

The paper's central results are external benchmark measurements (MiniF2F-test, ProofNet-test, ProverBench) obtained by sampling trained checkpoints, with no fitted parameter reused in the evaluation formula. Eq. (1)-(2) define the optimization objectives; Eq. (3)-(4) are standard DAPO policy updates. Rewards are simple verifier status rewards (plus explored fine-grained rewards that are explicitly reported as not beneficial), and the RL data selection band (pass@8 in 1/8-1/2) is a curriculum heuristic, not a fit to test-set scores. Self-citations to Leanabell-Prover-V1 appear only as background and as a baseline in Table 1, not as a load-bearing uniqueness or derivation argument. The main caveat is a confound, not circularity: Table 3's 'Vanilla' row (64.7% for KM without reflection) sits below the vanilla RL control (65.5%), so Table 2's headline comparison partly attributes inference-time verifier reflection to the RL training itself; similarly the cold-start SFT is not separately ablated. These are causal-attribution limitations, acknowledged in the Limitations section's discussion of diminishing benefits, and do not make the predictions equivalent to the inputs by construction.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new entities. Its free parameters are limited to reward magnitudes and a data-filtering band, both described as chosen by hand. The central claims rest on the soundness of Lean 4, accurate transcription of baseline numbers, and absence of dataset contamination, which are reasonable but not all explicitly verified in the text.

free parameters (2)
  • Reward values R_format, R_failed, R_success = 0.2, 1.0, 1.0
    Hand-chosen in Section 2.3; the authors report that a simple reward suffices, so the exact magnitudes are not fitted to the benchmark.
  • RL training data selection pass rate range = 1/8 to 1/2 pass@8
    Chosen in Section 2.3 to keep an active prompt set; problems that are too easy or too hard are excluded, which shapes the training distribution.
assumptions (4)
  • domain assumption Lean 4 verifier is sound: a proof that compiles is a correct proof in the system's logic.
    The entire reward signal and evaluation rely on Lean 4's correctness; this is standard in the field.
  • domain assumption The base models' reported benchmark numbers are accurate and comparable.
    Tables 1, 4, and 5 compare against numbers transcribed from prior papers; any inconsistency would alter the claimed improvements.
  • domain assumption Cold-start SFT data synthesized by Claude-3.7-Sonnet does not overlap with test sets.
    Section 2.2 builds training data from NuminaMath and base-model outputs; the authors do not report a contamination check against MiniF2F, ProofNet, or ProverBench.
  • standard math pass@k estimator is unbiased under the stated sampling procedure.
    Standard practice in the field, used by prior papers.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning." pith.science (2026). https://pith.science/paper/VKFY3A5T

@misc{pith2026250708649,
  author       = {Pith},
  title        = {Pith review of: Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VKFY3A5T}},
  note         = {Machine review of arXiv:2507.08649}
}
read the original abstract

We introduce our Leanabell-Prover-V2, a 7B large language models (LLMs) that can produce formal theorem proofs in Lean 4, with verifier-integrated Long Chain-of-Thoughts (CoT). Following our previous work Leanabell-Prover-V1, we continual to choose to posttrain existing strong prover models for further performance improvement. In our V2 version, we mainly upgrade the Reinforcement Learning (RL) with feedback provided by the Lean 4 verifier. Crucially, verifier feedback, such as indicating success or detailing specific errors, allows the LLM to become ``self-aware'' of the correctness of its own reasoning process and learn to reflexively correct errors. Leanabell-Prover-V2 directly optimizes LLM reasoning trajectories with multi-turn verifier interactions, together with feedback token masking for stable RL training and a simple reward strategy. Experiments show that Leanabell-Prover-V2 improves performance by 3.2% (pass@128) with Kimina-Prover-Preview-Distill-7B and 2.0% (pass@128) with DeepSeek-Prover-V2-7B on the MiniF2F test set. The source codes, curated data and models are available at: https://github.com/Leanabell-LM/Leanabell-Prover-V2.

Figures

Figures reproduced from arXiv: 2507.08649 by the authors.

Figure 10
Figure 10. | Lean 4 tactic power/automation levels [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  2. StepFun-Prover Preview: Let's Think and Verify Step by Step

    cs.AI 2025-07 conditional novelty 6.0 of 10

    A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.

Reference graph

Works this paper leans on

39 extracted references · 16 canonical work pages · cited by 2 Pith papers

  1. [1]

    Claude 3.7 Sonnet System card

    Anthropic. Claude 3.7 Sonnet System card. 2025. URL https://www.anthropic.com/ news/claude-3-7-sonnet

    work page 2025

  2. [2]

    Azerbayev, B

    Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023

    arXiv 2023

  3. [3]

    J. Beck. Offline rlaif: Piloting vlm feedback for rl via sfo. arXiv preprint arXiv:2503.01062, 2025

    work page arXiv 2025

  4. [4]

    Bhattacharya, S

    S. Bhattacharya, S. Badyal, T. Wheeler, S. Gil, and D. Bertsekas. Reinforcement learning for pomdp: Partitioned rollout and policy iteration with application to autonomous sequential repair problems. IEEE Robotics and Automation Letters, 5(3):3967–3974, 2020

    work page 2020

  5. [5]

    P . Coq. The coq proof assistant-reference manual.INRIA Rocquencourt and ENS Lyon, version, 5, 1996

    work page 1996

  6. [6]

    De Moura, S

    L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction (CAD), 2015

    work page 2015

  7. [7]

    G. Dong, K. Lu, C. Li, T. Xia, B. Yu, C. Zhou, and J. Zhou. Self-play with execution feedback: Improving instruction-following capabilities of large language models. arXiv preprint arXiv:2406.13542, 2024

    arXiv 2024

  8. [8]

    Dong and T

    K. Dong and T. Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025

    arXiv 2025

Show all 39 references
  1. [9]

    J. Feng, S. Huang, X. Qu, G. Zhang, Y. Qin, B. Zhong, C. Jiang, J. Chi, and W. Zhong. Retool: Reinforcement learning for strategic tool use in llms. arXiv preprint arXiv:2504.11536, 2025

    2025 arXiv

  2. [10]

    D. Guo, D. Yang, H. Zhang, J. Song, R. Zhang, R. Xu, Q. Zhu, S. Ma, P . Wang, X. Bi, et al. Deepseek-R1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025

    2025 arXiv

  3. [11]

    Huth and M

    M. Huth and M. Ryan. Logic in Computer Science: Modelling and reasoning about systems . Cambridge university press, 2004. 14

    2004

  4. [12]

    B. Jin, H. Zeng, Z. Yue, J. Yoon, S. Arik, D. Wang, H. Zamani, and J. Han. Search-r1: Training llms to reason and leverage search engines with reinforcement learning. arXiv preprint arXiv:2503.09516, 2025

    2025 arXiv

  5. [13]

    J. Li, E. Beeching, L. Tunstall, B. Lipkin, R. Soletskyi, S. C. Huang, K. Rasul, L. Yu, A. Jiang, Z. Shen, Z. Qin, B. Dong, L. Zhou, Y. Fleureau, G. Lample, and S. Polu. Numinamath, 2024

    2024

  6. [14]

    Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al. Goedel- prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025

    2025 arXiv

  7. [15]

    L. d. Moura and S. Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, 2021

    2021

  8. [16]

    Nipkow, M

    T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002

    2002

  9. [17]

    Parisi, Y

    A. Parisi, Y. Zhao, and N. Fiedel. Talm: Tool augmented language models. arXiv preprint arXiv:2205.12255, 2022

    2022 arXiv

  10. [18]

    S. G. Patil, T. Zhang, X. Wang, and J. E. Gonzalez. Gorilla: Large language model connected with massive apis. Advances in Neural Information Processing Systems (NeurIPS), 2024

    2024

  11. [19]

    C. Qian, E. C. Acikgoz, Q. He, H. Wang, X. Chen, D. Hakkani-Tür, G. Tur, and H. Ji. Toolrl: Reward is all tool learning needs. arXiv preprint arXiv:2504.13958, 2025

    2025 arXiv

  12. [20]

    Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025

    2025 arXiv

  13. [21]

    Schick, J

    T. Schick, J. Dwivedi-Yu, R. Dessì, R. Raileanu, M. Lomeli, E. Hambro, L. Zettlemoyer, N. Cancedda, and T. Scialom. Toolformer: Language models can teach themselves to use tools. Advances in Neural Information Processing Systems (NeurIPS), 2023

    2023

  14. [22]

    Z. Shao, P . Wang, Q. Zhu, R. Xu, J. Song, X. Bi, H. Zhang, M. Zhang, Y. Li, Y. Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024

    2024 arXiv

  15. [23]

    Shinn, F

    N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao. Reflexion: Language agents with verbal reinforcement learning. Advances in Neural Information Processing Systems (NeurIPS), 2023

    2023

  16. [24]

    H. Song, J. Jiang, Y. Min, J. Chen, Z. Chen, W. X. Zhao, L. Fang, and J.-R. Wen. R1- searcher: Incentivizing the search capability in llms via reinforcement learning. arXiv preprint arXiv:2503.05592, 2025

    2025 arXiv

  17. [25]

    K. Team, A. Du, B. Gao, B. Xing, C. Jiang, C. Chen, C. Li, C. Xiao, C. Du, C. Liao, et al. Kimi k1.5: Scaling reinforcement learning with llms. arXiv preprint arXiv:2501.12599, 2025

    2025 arXiv

  18. [26]

    Q. Team. Qwen2.5: A party of foundation models, September 2024. URL https://qwen lm.github.io/blog/qwen2.5/

    2024

  19. [27]

    Q. Team. Qwq-32b: Embracing the power of reinforcement learning, March 2025. URL https://qwenlm.github.io/blog/qwq-32b/. 15

    2025

  20. [28]

    Tsoukalas, J

    G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaud- huri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. arXiv preprint arXiv:2407.11214, 2024

    2024 arXiv

  21. [29]

    H. Wang, C. Qian, W. Zhong, X. Chen, J. Qiu, S. Huang, B. Jin, M. Wang, K.-F. Wong, and H. Ji. Otc: Optimal tool calls via reinforcement learning. arXiv preprint arXiv:2504.14870, 2025

    2025 arXiv

  22. [30]

    H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025

    2025 arXiv

  23. [31]

    R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024

    2024 arXiv

  24. [32]

    H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. Deepseek- prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024

    2024 arXiv

  25. [33]

    H. Xin, Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024

    2024 arXiv

  26. [34]

    Y. E. Xu, Y. Savani, F. Fang, and Z. Kolter. Not all rollouts are useful: Down-sampling rollouts in llm reinforcement learning. arXiv preprint arXiv:2504.13818, 2025

    2025 arXiv

  27. [35]

    S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao. React: Synergizing rea- soning and acting in language models. In International Conference on Learning Representations (ICLR), 2023

    2023

  28. [36]

    Q. Yu, Z. Zhang, R. Zhu, Y. Yuan, X. Zuo, Y. Yue, W. Dai, T. Fan, G. Liu, L. Liu, et al. Dapo: An open-source llm reinforcement learning system at scale. arXiv preprint arXiv:2503.14476, 2025

    2025 arXiv

  29. [37]

    Zhang, Q

    J. Zhang, Q. Wang, X. Ji, Y. Liu, Y. Yue, F. Zhang, D. Zhang, G. Zhou, and K. Gai. Leanabell- prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025

    2025 arXiv

  30. [38]

    Zheng, J

    K. Zheng, J. M. Han, and S. Polu. Minif2f: a cross-system benchmark for formal olympiad- level mathematics. arXiv preprint arXiv:2109.00110, 2021

    2021 arXiv

  31. [39]

    tactic power

    T. Ziegenbein, G. Skitalinskaya, A. B. Makou, and H. Wachsmuth. Llm-based rewriting of inappropriate argumentation using reinforcement learning from machine feedback. arXiv preprint arXiv:2406.03363, 2024. A. Cold-start Details As shown in Figure 7 and Figure 8, we present the...

    2024 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.