Pith. sign in

REVIEW 5 major objections 5 minor 3 cited by

MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation

T0 review · 5 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read The paper claims that a stepwise Lean prover using multi-perspective search reaches 75.82% on miniF2F and beats all 7B baselines on ProofNet.

desk verdict Engineered stepwise prover with a plausible data-curation recipe, but the multi-perspective search efficiency claim needs the BFS baseline fully specified before it can be trusted. read the letter →

arxiv 2505.10962 v1 pith:H6ZXNKDF submitted 2025-05-16 cs.AI

Zhenwen Liang , Linfeng Song , Yang Li , Tao Yang , Feng Zhang , Haitao Mi , Dong Yu This is my paper · ORCID
classification cs.AI
keywords automatedtheoremprovingLean4stepwiseproofsearchbest-firstmulti-perspectiveexpertiterationdatacurationformalmathematics
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

The paper argues that stepwise theorem proving in Lean can be made substantially stronger by fixing two weaknesses of existing search-based provers: reliance on a single learned critic and indiscriminate reuse of expert-iteration data. It claims that a multi-perspective tree search, which keeps one critic-chosen node and three heuristic-chosen nodes per expansion, plus a curation step that drops roughly 40% of short or low-value training proofs, raises the success rate to 75.82% on miniF2F (185 of 244 problems) and 32.97% on ProofNet with a 7-billion-parameter model. A careful reader would care because the proofs are machine-checked by the Lean compiler, and because the same search also finds materially shorter proofs (mean 3.44 steps versus 15.91 and 52.16 for two whole-proof provers on 170 shared problems).

What carries the argument

The load-bearing mechanism is the multi-perspective tree search. In each expansion the system samples tactic candidates and retains up to four next states: one selected by a learned critic that predicts distance-to-completion, and three selected by hand-designed heuristics: a tactic-effectiveness score favoring transformative tactics, minimizing the number of case splits, and preferring shorter Lean state strings. A separate data-curation pass supports the model by removing proofs of three or fewer steps and steps whose tactics produce no state change, cutting about 40% of training data with little effect on accuracy.

What would settle it

Run the same 7B model and the same critic in a pure best-first search with a total tactic-candidate budget $B$, and run MPS with the same sampling and iteration settings at a budget $B/4$; if BFS at pass@$4k$ matches or exceeds MPS at pass@$k$ on miniF2F, the central efficiency claim fails.

Watch

Extended reading notes

Core claim

The central claim, stated on the paper's own terms, is that MPS-Prover is the strongest published 7B stepwise prover on miniF2F and ProofNet. It proves 185 of 244 miniF2F problems under an accumulative search, a gain over the previous stepwise best (BFS-Prover at 72.54%), and reaches 32.97% on ProofNet, ahead of all 7B baselines including a CoT-distilled model. Under approximately matched computational budgets, MPS at pass@k is reported to beat BFS at pass@4k, with the gap widening as the budget grows. It also finds shorter and more tactic-diverse proofs than both the BFS baseline and whole-proof provers, which the paper attributes to combining multiple selection perspectives rather than trusting a single critic's bias.

Load-bearing premise

The load-bearing assumption is that comparing MPS at pass@k with BFS at pass@4k really does compare roughly equal computational budgets; the paper does not specify the BFS baseline's configuration, so if BFS was run with different trials, iteration counts, or sampling, the claimed efficiency gain could be an artifact.

Editorial extensions

If this is right

  • Within the 7B model class, a natively trained stepwise prover can beat whole-proof baselines, including a CoT-distilled one, on ProofNet.
  • Under the paper's budget-equivalence assumption, spending the same compute on multi-perspective expansion rather than more BFS trials yields higher accuracy at every budget tested.
  • About 40% of expert-iteration training data can be dropped without hurting proof-finding performance, making training cheaper.
  • Stepwise search produces dramatically shorter proofs, which are easier to inspect and verify, while whole-proof systems generate longer scripts on the same theorems.

Reading between the lines

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

  • If the budget-equivalence comparison holds under closer scrutiny, the same multi-perspective principle could be applied to other sparse tree searches to reduce wasted expansion.
  • The heuristic scoring table is manually tuned for Lean; a learned or automatically fitted version of these scores could transfer the idea to other proof assistants, but the paper does not test that.
  • The authors' hybrid-system suggestion implies a testable extension: feed MPS-Prover's short proof skeletons as high-level plans to a whole-proof generator.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 5 minor

Summary. This paper introduces MPS-Prover, a stepwise Lean 4 theorem prover built on Qwen2.5-Math-7B. Its two claimed contributions are (1) a post-training data curation strategy that removes approximately 40% of expert-iteration training data by filtering short proofs and ineffective tactic steps, and (2) a multi-perspective tree search that, in addition to a learned distance-prediction critic, selects nodes using three hand-designed heuristics: tactic effectiveness scoring, minimizing case splits, and shortest state preference. On miniF2F-test the system reports 75.82% accuracy under an accumulative protocol, compared with 72.54% for BFS-Prover, and reports 32.97% on ProofNet, surpassing several 7B baselines. The paper additionally reports that MPS produces shorter proofs than whole-proof baselines (mean 3.44 steps vs 15.91 and 52.16 on 170 common miniF2F problems) and more diverse proofs than its own BFS baseline. Generated proofs are ultimately checked by the Lean compiler, which guards against repl-level mis-verification.

Significance. If the empirical claims hold, this is a strong step-level 7B result on miniF2F and ProofNet, and the data-curation finding (roughly 40% data reduction with roughly equal performance) would be practically valuable. The use of a final Lean compiler check is a clear strength, and the proof-length analysis, while confounded by the search heuristics, addresses an under-studied axis of comparison. However, the paper's main methodological claim—that multi-perspective search is more efficient than BFS under equivalent budgets—rests on an underspecified baseline, and the headline differences (8 problems on miniF2F; 1–5 problems in ablations) are reported without any uncertainty quantification. Reproducibility is currently incomplete because no code, model weights, or detailed search configurations are provided. The central benchmark numbers are plausible, but the evidence for the search-specific efficiency advantage and for the contribution of individual heuristics is not yet fully established.

major comments (5)
  1. [Section 3.2, Figure 3] The central efficiency claim—'MPS consistently outperforms BFS when allocated similar computational resources'—requires BFS pass@4k to be budget-equivalent to MPS pass@k. This equivalence demands that BFS use the same LLM backbone, the same distance critic, the same Nmax_iter and Nsamples, and the same accumulative protocol. None of these are reported for Figure 3. The BFS rows in Table 1 use the notation '2048 × 2 × 600', whereas the MPS rows use '64 × 4 × 800 × 8', so the two budget formats are not obviously comparable. Please specify the exact BFS configuration used in Figure 3, report per-budget problem counts for both methods, and state whether the same critic and iteration limits were used.
  2. [Section 3.1, Table 1; Section 3.3, Table 3] The reported performance differences are small relative to the stochasticity of the sampling procedure. The headline improvement over BFS-Prover is 8 problems out of 244 (75.82% vs 72.54%), and each ablation row differs from the full method by only 1–5 problems. No repeated runs, random seeds, or confidence intervals are provided. Without these, the claim of a 'significant improvement' and the attribution of the ablations to specific heuristics are not quantitatively supported. Please report variance across multiple independent runs or otherwise demonstrate that the observed gaps exceed run-to-run noise.
  3. [Section 3.4, Figure 4] The proof-length and diversity analyses are confounded by the MPS heuristics themselves. The 'Shortest State Preference' and 'Minimizing Case Splits' heuristics directly bias the search toward simpler and shorter states, and the 'Tactic Effectiveness Scoring' favors goal-closing and transformative tactics, so shorter and less repetitive proofs are partly by construction rather than an emergent property of multi-perspective search. Furthermore, the comparison between MPS pass@64 and BFS pass@256 does not state the BFS Nmax_iter, Nsamples, or exact total budget, and restricting the analysis to 'commonly solved problems' introduces selection bias. Please report the exact budgets, analyze the full sets of solved problems, and, if the claim is about proof efficiency, compare with a BFS baseline that is matched on the aspects not under test.
  4. [Section 2.2, Filtering Short Proofs] The short-proof filtering threshold of 3 is selected by a grid search over {2, 3, 4, 5}. The paper does not state whether this grid search was performed on a held-out validation split or on the miniF2F test set. If the test set was used, the data-curation effectiveness claim (40% data reduction with no performance loss) could reflect selection on the evaluation benchmark. Please clarify the split used for the grid search and report the performance for the other thresholds.
  5. [Section 3.1, Table 2] Table 2 states that all models, including MPS-Prover, were evaluated under their 'respective maximum reported sampling budgets', but the actual budget used for MPS-Prover on ProofNet is not reported. Given the paper's budget formula Npass × Nperspectives × Nmax_iter × Nsamples, please report the values used for ProofNet, including whether the accumulative protocol was applied. Without this, the comparison to baselines such as DeepSeek-Prover-V2 is not fully reproducible.
minor comments (5)
  1. [Section 5] The word 'comfirms' should be 'confirms'.
  2. [Appendix A] The text attributes DeepSeek-Prover-V2 to 'Guo et al. (2025)', but the reference list identifies DeepSeek-Prover-V2 as Ren et al. (2025); the citation should be corrected.
  3. [Table 4] The procedure for selecting the '170 common miniF2F problems' is not described; please state how the common set was determined and whether it is the same set used in Section 3.4.
  4. [Appendix D] Several displayed Lean proofs contain LaTeX artifacts (e.g., '\mathbb{R}' rendered as 'R' and stray '£' characters in the DeepSeek-Prover V2 proof); these should be cleaned up for readability.
  5. [Section 3.2] The acronym BFS is used for Best-First Search, which can be confused with breadth-first search; a footnote or parenthetical clarification at first use would help readers unfamiliar with the step-proving literature.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: external benchmarks and disclosed heuristics; the BFS-budget comparison is under-specified but not an input-output identity.

full rationale

The paper's central claims are external benchmark success rates (miniF2F 75.82%, ProofNet 32.97%) verified by the Lean compiler, so they cannot reduce to fitted inputs or self-citations. The only self-cited component is the critic training ('Following Li et al. (2024b), our critic model is trained using a hierarchical, tree-based distance prediction method'), but Li et al. is prior work with overlapping authors and is cited as a method component, not as a uniqueness theorem or as evidence for MPS-Prover's accuracy. The proof-length comparison in Section 3.4 is partially designed into the algorithm ('Shortest State Preference. We prioritize tactics leading to shorter Lean 4 state strings'), but the paper explicitly presents this as a heuristic, and proof length in steps is not definitionally equal to state-string length; it is an algorithmic design objective, not a hidden fit. The Section 3.2 budget-equivalence comparison (MPS pass@k vs. BFS pass@4k) rests on an unstated assumption about BFS expanding one node per iteration with the same LLM, critic, and iteration count; this is an under-specified baseline and a reproducibility/efficiency-claim risk, but it is not circular because the comparison is an experimental protocol, not a derived quantity. No equation in the paper reduces the claimed predictions to their inputs, and no load-bearing argument is supported solely by a self-citation. Therefore no significant circularity.

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

The paper's central claims rest on the Lean environment, public math datasets, and the prior critic framework; they introduce no new entities. The main hand-chosen quantities are the filtering threshold, the tactic scoring table, and the search hyperparameters, none of which are given with sensitivity analysis.

free parameters (4)
  • Short-proof filtering threshold = 3
    Chosen by grid search over {2,3,4,5} to decide which proofs to remove from training data; removes about 40% of data. The paper does not state whether the grid search was evaluated on a validation split or on the test benchmarks.
  • Tactic Effectiveness scores = Table 5 in Appendix B
    Hand-assigned scores for tactics used by the Tactic Effectiveness heuristic to select nodes. These scores directly shape search behavior and are based on expert intuition rather than learned or validated values.
  • Number of search perspectives = 4
    One critic plus three heuristic rules; the paper fixes this to 4 without reporting sensitivity to the number of perspectives.
  • Search budget hyperparameters = Nsamples=8, Nmax_iter=800
    Defines total tactic candidates per pass (Npass x 4 x 800 x 8). No sensitivity analysis is reported for these values.
assumptions (4)
  • domain assumption The Lean 4 proof assistant and Mathlib formal library correctly certify the generated proofs.
    The final verification step relies on the Lean compiler's soundness; standard for this line of work.
  • domain assumption The public datasets (Lean Workbook, Numina, AoPS-Instruct) provide correctly formalized natural language problems for expert iteration.
    Section 2.1 uses these datasets as the source for autoformalization and proof collection without auditing their correctness.
  • domain assumption The repl tool and the hierarchical tree-based distance critic from HunyuanProver (Li et al., 2024b) work as reported.
    Section 2.3 builds on the critic training method from prior work with overlapping authors; its reliability is taken as given.
  • domain assumption The set of 244 miniF2F and 371 ProofNet test problems is a meaningful benchmark of proving ability.
    Standard benchmarks, but they constrain generalization claims to those distributions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation." pith.science (2026). https://pith.science/paper/H6ZXNKDF

@misc{pith2026250510962,
  author       = {Pith},
  title        = {Pith review of: MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/H6ZXNKDF}},
  note         = {Machine review of arXiv:2505.10962}
}
read the original abstract

Automated Theorem Proving (ATP) in formal languages remains a formidable challenge in AI, demanding rigorous logical deduction and navigating vast search spaces. While large language models (LLMs) have shown promising performance, existing stepwise provers often suffer from biased search guidance, leading to inefficiencies and suboptimal proof strategies. This paper introduces the Multi-Perspective Search Prover (MPS-Prover), a novel stepwise ATP system designed to overcome these limitations. MPS-Prover incorporates two key innovations: a highly effective post-training data curation strategy that prunes approximately 40% of redundant training data without sacrificing performance, and a multi-perspective tree search mechanism. This search integrates a learned critic model with strategically designed heuristic rules to diversify tactic selection, prevent getting trapped in unproductive states, and enhance search robustness. Extensive evaluations demonstrate that MPS-Prover achieves state-of-the-art performance on multiple challenging benchmarks, including miniF2F and ProofNet, outperforming prior 7B parameter models. Furthermore, our analyses reveal that MPS-Prover generates significantly shorter and more diverse proofs compared to existing stepwise and whole-proof methods, highlighting its efficiency and efficacy. Our work advances the capabilities of LLM-based formal reasoning and offers a robust framework and a comprehensive analysis for developing more powerful theorem provers.

Figures

Figures reproduced from arXiv: 2505.10962 by the authors.

Figure 1
Figure 1. Common failure patterns in step-based theorem provers. (a) Repetitive steps caused by [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Search-strategy comparison in Lean-based proving. (a) Best-First Search follows the single branch favoured by a learned critic; when that critic’s inherent bias selects an unprovable state or an ineffective tactic, the entire proof attempt terminates in failure. (b) Multi-Perspective Search (MPS) evaluates each expansion step from heuristics as well as the critic, preserving a more diverse set of promising Lean 4 st… view at source ↗
Figure 3
Figure 3. Performance comparison under equiva￾lent computational budgets [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Quantitative analysis of proof characteristics for commonly solved problems by BFS [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 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. Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

    cs.LO 2025-07 conditional novelty 6.0 of 10

    A decoupled reasoning-and-proving framework generated machine-verified Lean proofs for five post-2000 IMO problems.

  3. Mathesis: Towards Formal Theorem Proving from Natural Languages

    cs.AI 2025-06 conditional novelty 6.0 of 10

    An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.

Reference graph

Works this paper leans on

39 extracted references · 9 canonical work pages · cited by 3 Pith papers

  1. [1]

    Ai achieves silver-medal standard solving international mathematical olympiad problems.’25 july 2024, 2024

    DeepMind AlphaProof and AlphaGeometry Teams. Ai achieves silver-medal standard solving international mathematical olympiad problems.’25 july 2024, 2024

    work page 2024

  2. [2]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023

    arXiv 2023

  3. [3]

    Proofs and refutations, and z3

    Leonardo Mendon c a de Moura and Nikolaj S Bj rner. Proofs and refutations, and z3. In LPAR Workshops, volume 418, pp.\ 123--132. Doha, Qatar, 2008

    work page 2008

  4. [4]

    Stp: Self-play llm theorem provers with iterative conjecturing and proving

    Kefan Dong and Tengyu Ma. Stp: Self-play llm theorem provers with iterative conjecturing and proving. arXiv e-prints, pp.\ arXiv--2502, 2025

    2025

  5. [5]

    Formal theorem proving by rewarding llms to decompose proofs hierarchically

    Kefan Dong, Arvind Mahankali, and Tengyu Ma. Formal theorem proving by rewarding llms to decompose proofs hierarchically. arXiv preprint arXiv:2411.01829, 2024

    arXiv 2024

  6. [6]

    Baldur: Whole-proof generation and repair with large language models

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. 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, pp.\ 1229--1241, 2023

    2023

  7. [7]

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025

    arXiv 2025

  8. [8]

    Deepmath-deep sequence models for premise selection

    Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas E \'e n, Fran c ois Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016

    work page 2016

Show all 39 references
  1. [9]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Repr...

    2023

  2. [10]

    Hypertree proof search for neural theorem proving

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35: 0 26337--26349, 2022

    2022

  3. [11]

    Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions

    Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face reposito...

    2024

  4. [12]

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving

    Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024 b

    2024 arXiv

  5. [13]

    Goedel-prover: A frontier model for open-source automated theorem proving

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025

    2025 arXiv

  6. [14]

    Efficient neural theorem proving via fine-grained proof structure analysis

    Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and Andrew C Yao. Efficient neural theorem proving via fine-grained proof structure analysis. arXiv preprint arXiv:2501.18310, 2025

    2025 arXiv

  7. [15]

    Deep network guided proof search

    Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017

    2017 arXiv

  8. [16]

    Leveraging online olympiad-level math problems for llms training and contamination-resistant evaluation

    Sadegh Mahdavi, Muchen Li, Kaiwen Liu, Christos Thrampoulidis, Leonid Sigal, and Renjie Liao. Leveraging online olympiad-level math problems for llms training and contamination-resistant evaluation. arXiv preprint arXiv:2501.14275, 2025

    2025 arXiv

  9. [17]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction--CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12--15, 2021, Proceedings 28, pp.\ 625--635. Springer, 2021

    2021

  10. [18]

    Isabelle: A generic theorem prover

    Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994

    1994

  11. [19]

    Generative language modeling for automated theorem proving

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020

    2009 arXiv

  12. [20]

    Formal mathematics statement curriculum learning

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022

    2022 arXiv

  13. [21]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition

    ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025

    2025 arXiv

  14. [22]

    Vampire 1.1

    Alexandre Riazanov and Andrei Voronkov. Vampire 1.1. In Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena, Italy, June 18--22, 2001 Proceedings 1, pp.\ 376--380. Springer, 2001

    2001

  15. [23]

    Proving theorems recursively

    Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively. arXiv preprint arXiv:2405.14414, 2024 a

    2024 arXiv

  16. [24]

    Lego-prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In 12th International Conference on Learning Representations (ICLR 2024). Internati...

    2024

  17. [25]

    Kimina-prover preview: Towards large formal reasoning models with reinforcement learning

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025

    2025 arXiv

  18. [26]

    Premise selection for theorem proving by deep graph embedding

    Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017

    2017

  19. [27]

    Theoremllama: Transforming general-purpose llms into lean4 experts

    Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp.\ 11953--11974, 2024 c

    2024

  20. [28]

    Internlm2

    Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024

  21. [29]

    Deepseek-prover-v1

    Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi 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

  22. [30]

    Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving

    Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025

    2025

  23. [31]

    Leandojo: Theorem proving with retrieval-augmented language models

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36: 0 21573--21612, 2023

    2023

  24. [32]

    Lean workbook: A large-scale lean problem set formalized from natural language math problems

    Huaiyuan Ying, Zijian Wu, Yihan Geng, JIayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024

    2024

  25. [33]

    Leanabell-prover: Posttraining scaling in formal reasoning

    Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025

    2025 arXiv

  26. [34]

    Subgoalxl: Subgoal-based expert learning for theorem proving

    Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint arXiv:2408.11172, 2024

    2024 arXiv

  27. [35]

    minif2f: a cross-system benchmark for formal olympiad-level mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR, 2022

    2022

  28. [36]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

  29. [37]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should ...

  30. [38]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@firs...

  31. [39]

    yk ˔39s7 z !@ !@ !@ !O `],B B B B !@ !@ !@ !o j !@ !@ !@ !@ qA B B B - D\]C # B B B

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibset...

    2024

Pith tools

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