Pith. sign in

REVIEW 4 major objections 6 minor 40 references

LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

T0 review · 4 major / 6 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 feeding a language-model prover the factorized Lean proof state at each step more than doubles its success rate on MiniF2F, from 9.59% black-box whole-proof generation to 18.36% white-box rollouts.

desk verdict A genuinely useful open-source Lean 4 tool and dataset, with an honestly hedged experiment whose headline comparison does not isolate factorized states—worth publishing after protocol clarifications. read the letter →

arxiv 2507.14722 v1 pith:YZN6YGE4 submitted 2025-07-19 cs.LG cs.AI

Matěj Kripner , Michal Šustr , Milan Straka This is my paper
classification cs.LGcs.AI
keywords automatedtheoremprovingwhite-boxproofsearchfactorizedstatesLean4largelanguagemodelstreedatasetmetavariablecouplingMiniF2F
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 argues that a theorem-proving language model performs better when it can see the intermediate proof state — the list of open goals and hypotheses — at each step of a proof search, rather than only the original theorem. To test this, the authors built LeanTree, a tool that splits Lean 4 proof states into independent branches, and a dataset of such factorized states extracted from human-written proofs in the standard Lean library and from a large collection of autoformalized proofs. Using the Llemma-7B model on a corrected Lean 4 port of MiniF2F, ten linear rollouts in white-box mode solved 18.36% of problems, versus 9.59% for black-box whole-proof generation and 5.32% for black-box rollouts. The paper's central claim is that carefully exposing internal proof state, in factorized form, is what produces the gain.

What carries the argument

The central object is the factorized proof state: a Lean 4 proof state decomposed into its metavariable-independent goals, each with its target type and available hypotheses. The LeanTree tool drives Lean's interactive execution layer, applying tactics to individual goals, and it detects when two goals share an undecided metavariable so they stay coupled and are not split. To generate training data, a proof-tree builder converts human-written Lean proofs into trees whose nodes are such factorized states and whose edges are single tactic steps, simplifying nested tactics, splitting composite rw tactics, and adding synthetic case steps when needed. This factorization is what lets search operate on one independent goal at a time and is the mechanism the experiment isolates.

What would settle it

Re-run the MiniF2F comparison holding the prompt template, decoding settings, and the manual first-tactic selection identical across conditions, and include a third condition that receives the same state information in unfactorized form. If the factorized white-box condition no longer beats the unfactorized-state and black-box conditions, the result is an artifact of prompting or context differences rather than of factorized proof-state information.

Watch

Extended reading notes

Core claim

The paper's central claim is that white-box proof search with factorized proof states outperforms black-box generation in the setting tested. With ten independent linear rollouts of up to 25 tactic steps using Llemma-7B, white-box rollouts solved 18.36% ± 0.60 of MiniF2F problems, compared with 9.59% ± 0.71 for black-box whole-proof generation and 5.32% ± 0.37 for black-box rollouts. The paper attributes this to the factorized state representation, which reduces the policy's burden of tracking the proof state implicitly and lets the search tackle goals independently. It also reports that all proofs found are independently verified with the Lean kernel, and documents a verification fix that catches false-positive proofs that the REPL previously accepted.

Load-bearing premise

The gain in success rate is caused by the factorized proof-state information itself, not by incidental differences in the prompt format, parsing, or generation settings between the white-box and black-box conditions.

Editorial extensions

If this is right

  • If white-box rollouts with factorized states beat black-box generation, then access to intermediate proof states should be a first-class input in future theorem-proving LLM systems.
  • The dataset of factorized proof trees, with per-node proof size and depth, can serve as supervised data for training tactic-prediction and critic models.
  • LeanTree's handling of metavariable coupling means proof search can parallelize across independent branches without risking invalid proofs.
  • The new incremental verification strategy, checking only newly introduced assignments, both prevents false-positive proofs and reduces verification time from quadratic to linear.
  • Black-box linear rollouts scoring below whole-proof generation suggests that forcing a model to commit to one tactic at a time without state feedback hurts; white-box state restores the benefit of incremental search.

Reading between the lines

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

  • The result suggests that part of the advantage of large reinforcement-learning-trained provers may come from implicitly learning state tracking, and factorized state input could give smaller models a cheaper route to the same capability.
  • A straightforward testable extension would be to fine-tune a model on the released factorized dataset and measure whether the gap widens further, since the experiments use a frozen pretrained model.
  • The verification false-positive fix implies that some previously reported results that rely on library-search tactics may have been inflated, and applying the same check to other prover outputs could surface hidden invalid proofs.
  • The dataset's node-level proof sizes and depths enable training critics for best-first search, potentially pushing white-box performance toward the reported 26.23% upper bound.
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

4 major / 6 minor

Summary. The paper presents LeanTree, a Lean 4 toolchain and dataset for white-box theorem proving. It provides a programmatic interaction module for proof search over factorized proof states, with detection of metavariable coupling, and a data extraction pipeline that converts existing Lean proofs into simplified proof trees. The authors release the tool and a dataset of over 100k factorized tactic proofs from Mathlib and DeepSeek-Prover-V1. In a preliminary experiment on MiniF2F with Llemma-7B, white-box linear rollouts solve 18.36% ± 0.60 of problems, versus 9.59% ± 0.71 for black-box whole-proof generation and 5.32% ± 0.37 for black-box linear rollouts; the paper concludes that supplying the prover with internal proof states improves proof search performance.

Significance. LeanTree fills a real infrastructure gap in the neural theorem proving community: unlike Evariste, it is released, works in Lean 4, and builds on community-maintained tooling (Lean REPL). The dataset of factorized proof trees and the proposed incremental kernel verification strategy are potentially valuable resources. The paper also identifies a concrete false-positive failure mode with the apply? tactic and confirms the need for independent proof verification. However, the headline empirical claim is preliminary and, as detailed below, the reported comparisons do not isolate the effect of factorized proof states. If the suggested ablations confirm the effect, the result would be a notable step toward white-box LLM provers. As it stands, the primary significance is the infrastructure contribution, not the empirical finding.

major comments (4)
  1. [Section 6, Figure 3] The white-box rollout condition differs from both black-box baselines along at least three axes: (i) the model observes the current proof state (open goals and hypotheses), (ii) the state is factorized into independent goals, and (iii) the prover receives verifier feedback after each tactic and can adapt. No condition presents the full unfactorized goal list to the model, and no black-box condition provides error-only feedback without state. Consequently, the sentence in Section 6, "supplying the prover with internal proof states improves proof search performance," is not directly supported by the reported comparison. The 18.36% versus 5.32% gap could be driven by iterative feedback alone, and the title's "factorized states" claim is not tested. Please add an unfactorized white-box control (i.e., the state rendered as a flat list of all open goals with their hypotheses) and a black-box condition that observes whether a tactic is accepted, or explicitly restrict the conclusion to the combined effect.
  2. [Appendix C / Section 6] The experimental protocol is underspecified. The paper does not state (a) the exact serialization of the factorized state, including how goals, hypotheses, and metavariables are rendered and whether all goals or only the main goal are shown, (b) the decoding parameters (temperature, top-p, max tokens, number of samples per prompt), (c) how the "first tactic" is extracted from a model output that may contain multiple tactics, comments, or natural-language text, or (d) how invalid tactics are handled during rollouts (e.g., skipped, terminate the rollout, or retry). Appendix C gives only a generic prompt and says the first tactic is selected manually. These details are necessary for reproducibility and for ruling out that the reported difference is an artifact of prompt formatting or decoding choices. Please provide complete prompts and generation settings for all three conditions.
  3. [Section 6 (black-box rollout baseline)] The black-box rollout baseline is a blind sequence generator: the model never sees the result of a tactic, so it is effectively generating an open-loop tactic sequence. The low success rate of 5.32% may reflect the difficulty of unconstrained sequence generation rather than the absence of proof-state information. To separate the value of state information from the value of verifier feedback, at minimum report per-step tactic acceptance rates for both rollout conditions, and ideally compare against a black-box baseline that is allowed to restart or revise after a verifier error. This concern is load-bearing for the central empirical claim.
  4. [Sections 1, 4, and 6] The experiments do not use the LeanTree dataset or the factorized proof-tree representation at all; they apply off-the-shelf Llemma-7B in a simple linear rollout. Thus the paper's two main contributions—the tool/dataset and the empirical comparison—are disconnected. The claim that factorization accelerates proof search would be much stronger if the dataset were used (e.g., for fine-tuning or retrieval) or if the search algorithm exploited factorization for parallel exploration. Please clarify how the reported results relate to the proposed factorization, or adjust the framing to be about white-box state access rather than the specific LeanTree factorization.
minor comments (6)
  1. [Section 6 (hardware description)] "192 CPU nodes" should presumably be "192 CPU cores" or "192 logical processors"; please correct.
  2. [Figure 2 caption] The synthetic nodes and edges are marked with a dashed border in the figure, but the caption does not define the dashed-border notation; please add an explanation in the caption or in the main text.
  3. [Section 4.2] The conversion-failure percentages (23.0% for Mathlib and 4.7% for DeepSeek-Prover-V1) are reported without a breakdown by failure category; since calc and conv account for 28.6% of Mathlib failures, please provide the remaining major categories or state that the rest are other/unknown.
  4. [Appendix A] The statement that DeepSeek-Prover-V2 proofs "are thus incorrect" is supported by two named examples; it would be more precise to say "can be incorrect" or to provide a systematic check over the benchmark.
  5. [Appendix D (dataset schema)] The file names "lean-trees mathlib.jsonl" and "lean-trees deepseek-prover-v1.jsonl" appear to contain spaces; if this is intentional, clarify, otherwise rename them consistently (e.g., "leantrees-mathlib.jsonl").
  6. [Figure 3] The "best-first search" bar is from Azerbayev et al. (2023b) and is not an experiment in this paper; the caption should state this clearly and note whether the same model, search budget, and evaluation procedure were used.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper's central claim is an empirical comparison against the external MiniF2F benchmark, not a derivation that reduces to its inputs.

full rationale

LeanTree is an empirical systems paper. Its load-bearing claim, stated in Section 6, is that 'supplying the prover with internal proof states improves proof search performance,' supported by measured MiniF2F success rates: white-box rollout 18.36% ± 0.60, black-box whole-proof generation 9.59% ± 0.71, and black-box rollout 5.32% ± 0.37, all with the same Llemma-7B model. This is an experiment against an external benchmark, and no equation or parameter in the paper is defined in terms of the reported outcome. The factorization tooling is described as a system contribution, and the performance gain is not derived from the factorization definition itself; it is observed in a controlled comparison. The paper contains no fitted parameter later renamed as a prediction, no uniqueness theorem imported from the authors' own prior work, and no ansatz smuggled in via self-citation. The only self-referential-looking elements are citations to prior white-box work (Lample et al. 2022, Gloeckle et al. 2024), and these are not stated by the authors as their own results nor used to establish the MiniF2F numbers. The skeptic's concern that the experiment does not isolate factorization as a variable — because the white-box condition differs from black-box baselines in state access, iterative feedback, and factorization simultaneously — is a threat to internal validity or causal attribution, not circularity under the stated rules. Accordingly, the honest finding is no significant circularity, score 0.

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

No new physical entities are introduced. The only hand-chosen numbers are the experimental search budget (N, M). The central claim rests on Lean's soundness, the validity of goal factorization, the completeness of metavariable-coupling detection, and the representativeness of MiniF2F.

free parameters (2)
  • Number of rollouts N = 10
    Search budget per theorem; chosen by the authors, not optimized or fitted to the benchmark.
  • Maximum tactic steps M = 25
    Rollout length cap; chosen by the authors.
assumptions (5)
  • standard math The Lean 4 kernel is sound: proofs accepted by Lean are valid.
    The paper relies on Lean for final verification of proofs (Section 3.4, Appendix B).
  • domain assumption Independent goals can be proven in any order and the results combined into a proof of the conjunction.
    Foundation of factorization in Section 3.2; relies on metavariable instantiation in dependent type theory.
  • domain assumption Metavariable sharing is the only source of dependence between goals and LeanTree's detection of shared metavariables is complete.
    Section 3.3 assumes that detecting shared metavariables suffices to prevent unsafe factorization.
  • domain assumption MiniF2F (Lean 4 port by Wu et al.) is a representative benchmark for general theorem proving.
    The central comparison is performed on this benchmark only (Section 6).
  • ad hoc to paper The Llemma-7B model can in principle use the factorized state format despite not being trained on it.
    The experiment's positive result requires that the model finds the state information useful; this is an empirical premise of the specific setup.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4." pith.science (2026). https://pith.science/paper/YZN6YGE4

@misc{pith2026250714722,
  author       = {Pith},
  title        = {Pith review of: LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YZN6YGE4}},
  note         = {Machine review of arXiv:2507.14722}
}
read the original abstract

Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.

Figures

Figures reproduced from arXiv: 2507.14722 by the authors.

Figure 1
Figure 1. Example of an AND-OR proof tree for Theorem [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Proof tree builder in LeanTrees transforms a Lean proof with complex structure (left) into a proof tree (right) with [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Performance on MiniF2F using linear rollouts with Llemma-7B. Error bars show standard deviation over 5 runs. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

40 extracted references · 20 canonical work pages

  1. [1]

    and Tenev, V

    Achim, T. and Tenev, V. Harmonic: Building mathematical superintelligence. https://harmonic.fun/, 2023. Accessed: 2025-05-14

    work page 2023

  2. [2]

    Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4

    Aniva, L., Sun, C., Miranda, B., Barrett, C., and Koyejo, S. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. arXiv preprint arXiv:2410.16429, 2024

    arXiv

  3. [3]

    A proof-producing compiler for blockchain applications

    Avigad, J., Goldberg, L., Levit, D., Seginer, Y., and Titelman, A. A proof-producing compiler for blockchain applications. J. Autom. Reason., 69 0 (2), April 2025. ISSN 0168-7433. doi:10.1007/s10817-025-09723-y. URL https://doi.org/10.1007/s10817-025-09723-y

    doi:10.1007/s10817-025-09723-y 2025

  4. [4]

    W., Radev, D., and Avigad, J

    Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. Proof N et: Autoformalizing and formally proving undergraduate-level mathematics (2023). URL https://arxiv. org/abs/2302.12433, 2023 a

    arXiv 2023

  5. [5]

    D., McAleer, S., Jiang, A

    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 mathematics. arXiv preprint arXiv:2310.10631, 2023 b

    arXiv 2023

  6. [6]

    The description logic handbook: Theory, implementation and applications

    Baader, F. The description logic handbook: Theory, implementation and applications. Cambridge university press, 2003

    work page 2003

  7. [7]

    and Tinelli, C

    Barrett, C. and Tinelli, C. Satisfiability modulo theories. Handbook of model checking, pp.\ 305--343, 2018

    work page 2018

  8. [8]

    P., Sharlin, S., Feyzishendi, P., Dang, A

    Bobbin, M. P., Sharlin, S., Feyzishendi, P., Dang, A. H., Wraback, C. M., and Josephson, T. R. Formalizing chemical physics using the lean theorem prover. Digital Discovery, 3 0 (2): 0 264--280, 2024

    work page 2024

Show all 40 references
  1. [9]

    Axiomatic foundations and algorithms for deciding semantic equivalences of sql queries

    Chu, S., Murphy, B., Roesch, J., Cheung, A., and Suciu, D. Axiomatic foundations and algorithms for deciding semantic equivalences of sql queries. Proc. VLDB Endow., 11 0 (11): 0 1482–1495, July 2018. ISSN 2150-8097. doi:10.14778/3236187.3236200. URL https://doi.org/10.14778/3...

    2018

  2. [10]

    Lean 4 repl

    Community, L. Lean 4 repl. https://github.com/leanprover-community/repl, 2025. Accessed: 2025-04-28

    2025

  3. [11]

    The lean mathematical library

    Community, M. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp.\ 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi:10.1145/3372885.3373824. ...

    2020

  4. [12]

    Cryptography experiments in lean 4: SHA -3 implementation

    Doussot, G. Cryptography experiments in lean 4: SHA -3 implementation. Cryptology ePrint Archive, Paper 2024/1880, 2024. URL https://eprint.iacr.org/2024/1880

    2024

  5. [13]

    N., Ringer, T., and Brun, Y

    First, E., Rabe, M. N., Ringer, T., and Brun, Y. 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

  6. [14]

    Gelernter, H. L. Realization of a geometry theorem-proving machine. In Proceedings of the First International Conference on Information Processing (IFIP), pp.\ 273--281, 1959

    1959

  7. [15]

    ABEL : Sample efficient online reinforcement learning for neural theorem proving

    Gloeckle, F., Limperg, J., Synnaeve, G., and Hayat, A. ABEL : Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024

    2024

  8. [16]

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

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

    2025 arXiv

  9. [17]

    M., Rute, J., Wu, Y., Ayers, E

    Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Polu, S. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021

    2021 arXiv

  10. [18]

    Handbook of practical logic and automated reasoning

    Harrison, J. Handbook of practical logic and automated reasoning. Cambridge University Press, 2009

    2009

  11. [19]

    Jiang, D., Fonseca, M., and Cohen, S. B. Leanreasoner: Boosting complex logical reasoning with lean. North American Chapter of the Association for Computational Linguistics, 2024. doi:10.48550/arxiv.2403.13312

    2024 doi arXiv

  12. [20]

    and Kovsharov, A

    Karunus, E. and Kovsharov, A. Paperproof: A new proof interface for lean 4. https://github.com/Paper-Proof/paperproof, 2024. URL https://github.com/Paper-Proof/paperproof. Accessed: 2025-04-30

    2024

  13. [21]

    and Szepesv \'a ri, C

    Kocsis, L. and Szepesv \'a ri, C. Bandit based monte-carlo planning. In European conference on machine learning, pp.\ 282--293. Springer, 2006

    2006

  14. [22]

    Hypertree proof search for neural theorem proving

    Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35: 0 26337--26349, 2022

    2022

  15. [24]

    and Wheeler, D

    Megill, N. and Wheeler, D. A. Metamath: a computer language for mathematical proofs. Lulu. com, 2019

    2019

  16. [25]

    lean-training-data: Tools for extracting training‑data from lean libraries

    Morrison, K. lean-training-data: Tools for extracting training‑data from lean libraries. https://github.com/kim-em/lean-training-data, 2023. Accessed: 2025‑07‑01

    2023

  17. [26]

    Moura, L. d. and Ullrich, S. The L ean 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

  18. [27]

    and Sutskever, I

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

    2009 arXiv

  19. [28]

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

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

    2025 arXiv

  20. [29]

    Formalization of physics index notation in lean 4

    Tooby-Smith, J. Formalization of physics index notation in lean 4. ArXiv, abs/2411.07667, 2024. URL https://api.semanticscholar.org/CorpusID:273970152

    2024 arXiv

  21. [30]

    H., Wu, Y., Le, Q

    Trinh, T. H., Wu, Y., Le, Q. V., He, H., and Luong, T. Solving olympiad geometry without human demonstrations. Nature, 625 0 (7995): 0 476--482, 2024

    2024

  22. [31]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition

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

    2024 arXiv

  23. [32]

    Formalising the h-principle and sphere eversion

    van Doorn, F., Massot, P., and Nash, O. Formalising the h-principle and sphere eversion. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pp.\ 121–134, New York, NY, USA, 2023. Association for Computing Machinery. ISBN...

    2023

  24. [33]

    D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., et al

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

    2025 arXiv

  25. [34]

    Holophrasm: a neural automated theorem prover for higher-order logic

    Whalen, D. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016

    2016 arXiv

  26. [35]

    Internlm2

    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 on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024

    2024

  27. [36]

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data

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

    2024 arXiv

  28. [37]

    Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search

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

    2024 arXiv

  29. [38]

    J., and Anandkumar, A

    Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A. Lean D ojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36: 0 21573--21612, 2023

    2023

  30. [39]

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

    Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., and Chen, K. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024 a

    2024 arXiv

  31. [40]

    Internlm-math: Open math large language models toward verifiable reasoning

    Ying, H., Zhang, S., Li, L., Zhou, Z., Shao, Y., Fei, Z., Ma, Y., Hong, J., Liu, K., Wang, Z., et al. Internlm-math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024 b

    2024 arXiv

  32. [41]

    M., and Polu, S

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

    2021 arXiv

Pith tools

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