Pith. sign in

REVIEW 4 major objections 4 minor 33 references

Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques

T0 review · 4 major / 4 minor · reviewed 2026-08-09 · deepseek-v4-flash

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

Pith's one-line read By pairing an off-the-shelf language model with two simple proof-search strategies, the paper claims a 31.15% pass rate on the miniF2F benchmark—higher than every published single-attempt prover it compares with except one that uses a far…

desk verdict A simple ChatGPT+search baseline that's competitive but overclaims: ignore the 'surpasses all benchmarks' line, the real story is a reproducible no-fine-tuning setup with decent results and honest caveats. read the letter →

arxiv 2502.03321 v3 pith:B57BTCCN submitted 2025-02-05 cs.LO cs.AI

Sangjun Han , Taeil Hur , Youngmi Hur , Kathy Sangkyung Lee , Myungyoon Lee , Hyojae Lim This is my paper · ORCID
classification cs.LOcs.AI
keywords mathematicalreasoningformalproofgenerationsearchlargelanguagemodelLeanminiF2Fpass@kChatGPT
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 asks whether formal proof generation can be made much simpler than the current state of the art: instead of fine-tuning on proof corpora, use an off-the-shelf ChatGPT model and wrap it in basic search. The central empirical claim is that the resulting Lean-based system, bChatLean combined with dChatLean+, solves 76 of 244 miniF2F test theorems for a 31.15% pass@k rate, surpassing all published pass@1 benchmarks in its comparison and trailing only HyperTree, which uses a far larger sample budget. The authors also report 21 theorems not previously proved in the miniF2F repository, and comparable results on ProofNet, on 2023 AMC 12 problems, and with the Llemma model. If these numbers hold, they show that expensive training and elaborate search are not necessary to be competitive, and that prompt-plus-search design is a productive direction.

What carries the argument

The load-bearing mechanism is the pairing of a greedy depth-first search with a failure-memory feedback set called Bad(O), originally proposed for COPRA and adapted so that it stores tactic-state and failed-tactic pairs rather than just failed tactics; when the d-search restarts from the initial state, it consults Bad(O) to avoid retrying known failures. Complementing this, the b-search generates 64 tactics per tactic state with deduplication and temperature control. The two searches are deliberately complementary: the breadth-first pass covers many tactic directions cheaply, while the depth-first pass with Bad(O) revisits the proof from scratch to find paths that the breadth-first pass misses. The 31.15% result is the union of their proofs under the k=1, n=64 and k=50, n=1 configurations.

What would settle it

Recompute the pass rate under a single, shared protocol—for example, k=1 with 64 tactic samples per state and no second 50-attempt depth-first pass—and compare it with the same protocol for the prior systems; if bChatLean alone (29.10%) falls below the previous best single-attempt result, then the 'surpasses all benchmarks' headline does not survive a matched-budget comparison.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central discovery is that a fine-tuning-free ChatGPT model can reach state-of-the-art-level formal proof performance when paired with the right simple search. The b-search samples 64 tactics per Lean tactic state in a breadth-first style; the d-search samples one tactic greedily per attempt and, when it fails, restarts the whole proof from scratch, with a Bad(O) memory that records failed tactic-state/tactic pairs so it does not repeat them. Combining the two—bChatLean at k=1, n=64 and dChatLean+ at k=50, n=1—produces the 31.15% pass@k on miniF2F: 56 theorems solved by both, 15 only by bChatLean, and 5 only by dChatLean+. The paper also shows that 21 of the solved theorems were not in the recent miniF2F GitHub repository, indicating new proof artifacts. The authors take this as evidence that simple, reproducible models can be competitive with specialized theorem provers.

Load-bearing premise

The headline comparison assumes that the combined model's 31.15% pass@k, built from two runs with different attempt budgets (1 for bChatLean and 50 for dChatLean+), can be fairly compared with the pass@1 numbers reported for other systems, so that the paper's effective attempt budget is not much larger than theirs.

Editorial extensions

If this is right

  • If the 31.15% pass@k is correct and comparable, then a fine-tuning-free ChatGPT-based model is the best single-attempt-scale prover on miniF2F, ahead of specialized models like ReProver, DS-Prover, and COPRA.
  • Because 21 solved theorems were absent from the miniF2F repository, the method is not merely memorizing published proofs and can contribute new formal proofs.
  • The Llemma-based analogs (bLlemLean combined with dLlemLean+) reach 28.28%, beating Llemma's reported 26.23%, so the search algorithms transfer to a different base language model.
  • On ProofNet the combined model proves 46 of 350 theorems (13.14%), and on 2023 AMC 12 problems published after ChatGPT's training it solves 23.07%, suggesting the approach works outside miniF2F and on unseen problems.
  • The ablations show that raising temperature from 0.7 to 1.4 and increasing the number of attempts k improve pass rates, so output diversity is a first-order lever for this method.

Reading between the lines

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

  • If the pass@k comparison is accepted, a corollary not drawn by the paper is that the incremental value of domain-specific fine-tuning and reinforcement learning may be smaller than commonly assumed, since search budget and prompt design can close much of the gap.
  • The Bad(O) mechanism is essentially a tabu-style memory; extending it to rank or reweight remembered failures, or to forget failures after they become stale, is a natural testable next step that the paper does not explore.
  • The 21 newly proved theorems imply the pipeline can act as a proof-artifact generator; a direct extension would be to run the same system on the full set of currently unproved miniF2F problems and publish the resulting Lean proofs.
  • Because the headline comparison aggregates two unequal attempt budgets, a fairer benchmark would fix a single total sample budget per problem for all methods; the current design likely overstates the no-fine-tuning advantage.
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 / 4 minor

Summary. The paper proposes two simple proof-search algorithms, b-search and d-search, that wrap ChatGPT (GPT-4/GPT-4 Turbo) without fine-tuning to generate Lean proofs. On the miniF2F test set, the best configuration, an ensemble of bChatLean (k=1, n=64) and dChatLean+ (k=50, n=1), is reported to achieve a 31.15% pass rate, with 76 of 244 theorems solved. Additional experiments cover ProofNet, 2023 AMC 12 problems, and a transfer to the Llemma model, along with ablations on temperature, the number of attempts k, and the Bad(O) feedback mechanism. The abstract claims that this result 'surpasses all known benchmarks,' but Section 4.2 and Table 1 show that HyperTree reaches 41.0% and that the paper's own text concedes this exception.

Significance. If the empirical results are correct, the paper makes a useful contribution by showing that a fine-tuning-free ChatGPT wrapper with simple breadth-first and depth-first search can reach levels of performance on miniF2F comparable to several specialized theorem-proving systems. The proofs are machine-checked by Lean, and the authors provide code, ablations, and a post-training-cutoff AMC 12 evaluation that partially addresses contamination concerns. These are real strengths. However, the headline claim of 'surpassing all known benchmarks' is contradicted by the paper's own Table 1, and the combined 31.15% figure is not a standard pass@k metric. The significance of the work therefore depends on whether the authors can reframe their contribution as 'competitive under a clearly specified search budget' rather than as a new state-of-the-art result.

major comments (4)
  1. [Abstract and §4.2, Table 1] The abstract states that 'our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate,' but Table 1 lists HyperTree at 41.0%, and §4.2 explicitly says the pass rate 'surpasses all values in Table 1 except for in the case of the HyperTree model.' This is an internal contradiction in the central claim of the paper. The authors should correct the abstract to match the paper's own results, for example by saying 'surpasses all previously reported pass@1 results' or by excluding HyperTree from the comparison.
  2. [§4.2, Table 1] The 31.15% figure is the union of two heterogeneous search policies: bChatLean with k=1, n=64, and dChatLean+ with k=50, n=1. A pass@k rate is defined as the proportion of problems solved within a fixed number k of attempts under a single policy. The union of a k=1 policy and a k=50 policy is therefore not a standard pass@k and is not directly comparable to the pass@1 entries for PACT, Expert Iteration, ReProver, DS-Prover, Llemma, and COPRA in the same table. The authors should either report a single-policy pass@1 for their models, or clearly label the combined result as an ensemble under an explicit total attempt budget and avoid comparing it with pass@1 values.
  3. [§5, 'Considering challenging problems', and §4.4] The paper directly acknowledges that the Bernoulli inequality problem was solved by calling the pre-existing theorem one_add_mul_le_pow and that 'the model may have leveraged prior exposure to the library during training.' This raises a legitimate concern that part of the miniF2F pass rate reflects memorization of standard benchmark problems rather than general proof-search capability. The AMC 12 evaluation in §4.4 is a good step toward addressing this, but it is limited to 26 problems. The authors should either strengthen the contamination-resistance evidence or temper the claim that the miniF2F result demonstrates a general proof-generation ability.
  4. [§4.4, 'On ProofNet'] The paper says the ProofNet result (13.14%) is 'comparable to established benchmarks,' but no prior ProofNet pass-rate baselines are given. Without such numbers, this claim is unsupported. The authors should either provide relevant comparisons from prior work or remove the word 'comparable.'
minor comments (4)
  1. [§4.2, Table 1] The sample-budget notation is confusing: the table uses expressions such as '1 × 8 × 512' for PACT, '64 × 5000' for HyperTree, and '1 × 64 × −' for bChatLean, but the text does not clearly define e for their own runs or explain why '−' appears only in their rows. A brief clarifying sentence would help.
  2. [§4.2] The sentence 'Since the two proof searches described above use separate strategies to find proofs, we expect that combining the two models will open up room for a wider range of tactics to explore' is a reasonable intuition, but the paper does not quantify the expected gain or test the combination against a simple 'double the k' baseline. A short discussion of this alternative would strengthen the ensemble result.
  3. [§4.4, 'Using Llemma'] The claim that bLlemLean & dLlemLean+ 'surpassing the benchmark of 26.23% previously reported for Llemma' is interesting, but the paper does not state the number of attempts k or the sample budget used for the Llemma experiments in Table 6. Without this information, the comparison to the Llemma baseline is not fully interpretable.
  4. [General] The paper uses the terms 'b-search' and 'd-search' without formally defining them as algorithms in pseudocode or a formal specification. Given that the main contribution is algorithmic, a concise pseudocode listing for b-search and d-search would improve reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the 31.15% figure is an observed union of two search runs; concerns over the nonstandard pass@k label and possible pretraining exposure are benchmarking/validity issues, not self-referential reductions.

full rationale

This paper is an empirical benchmark study rather than a derivation, so the standard circularity patterns do not apply. The central result, 31.15%, is directly read off from running bChatLean and dChatLean+ on the 244 miniF2F test problems: the paper reports 56 theorems solved by both, 15 by bChatLean alone, and 5 by dChatLean+ alone, giving 76/244 = 31.15%. No fitted parameter is renamed as a prediction, no result is defined in terms of the claim it is supposed to support, and no load-bearing uniqueness theorem or self-citation chain is invoked. The legitimate concerns are comparability and reporting accuracy: the table labels the combined model as pass@k with k = '1 & 50', which is not a standard pass@k with a fixed number of attempts under one policy, and the abstract's statement that the model 'surpasses all known benchmarks' is contradicted by the same table's HyperTree row (41.0%). These are methodological weaknesses, not circularity. Likewise, the Bernoulli inequality discussion is an external-validity caveat about possible pretraining memorization, and the authors explicitly acknowledge it and compensate with post-cutoff AMC 12 problems; it does not make the reported pass rate a restatement of its own inputs. No circular step is therefore identifiable.

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

The central claim is an empirical benchmark result, so the ledger is dominated by evaluation assumptions rather than mathematical axioms. The main free parameters are search hyperparameters tuned on the evaluation data. The most fragile entries are the ad-hoc assumptions about benchmark comparability and pretraining contamination, both of which the paper partially acknowledges.

free parameters (4)
  • temperature = 1.4
    The main results use ChatGPT temperature T=1.4 after ablations showing higher pass rates than T=0.7; this value is chosen by hand and affects tactic diversity.
  • number of attempts k = 50 (d-search)
    dChatLean and dChatLean+ use up to 50 restart attempts per theorem; ablations show k=50 outperforms k=10 and k=1, so it is tuned on the evaluation set.
  • tactic samples n = 64 (b-search)
    b-search sets ChatGPT's n hyperparameter to 64, mirroring beam widths in ReProver; chosen as a practical budget rather than derived.
  • number of few-shot examples = 5
    Five examples from miniF2F validation are used in prompts; the specific examples are not enumerated, so this selection is not independently reproducible.
assumptions (4)
  • domain assumption Lean kernel and mathlib are sound
    Section 2.1: the paper treats Lean-verified proofs as ground truth; if the kernel or library contained unsoundness, pass rates would not certify correctness.
  • domain assumption miniF2F formalizations correctly encode the intended informal problems
    Section 2.2: miniF2F is taken as a standard benchmark without auditing each statement; a misformalized problem would make the corresponding proof trivial or irrelevant.
  • ad hoc to paper ChatGPT has no differential access to miniF2F solutions through pretraining
    Section 5 (Bernoulli inequality): the authors themselves suspect prior exposure to the Lean library, which would inflate the memorization component of the pass rate; this assumption is necessary for the claim that the method performs general proof search.
  • ad hoc to paper Combined pass@k is a meaningful comparability metric
    Section 4.2, Table 1: the headline 31.15% concatenates a single bChatLean run and 50 dChatLean+ restarts; the paper assumes this union is comparable to pass@1 baselines, which is not standard.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques." pith.science (2026). https://pith.science/paper/B57BTCCN

@misc{pith2026250203321,
  author       = {Pith},
  title        = {Pith review of: Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/B57BTCCN}},
  note         = {Machine review of arXiv:2502.03321}
}
read the original abstract

The challenge of formal proof generation has a rich history, but with modern techniques, we may finally be at the stage of making actual progress in real-life mathematical problems. This paper explores the integration of ChatGPT and basic searching techniques to simplify generating formal proofs, with a particular focus on the miniF2F dataset. We demonstrate how combining a large language model like ChatGPT with a formal language such as Lean, which has the added advantage of being verifiable, enhances the efficiency and accessibility of formal proof generation. Despite its simplicity, our best-performing Lean-based model surpasses all known benchmarks with a 31.15% pass rate. We extend our experiments to include other datasets and employ alternative language models, showcasing our models' comparable performance in diverse settings and allowing for a more nuanced analysis of our results. Our findings offer insights into AI-assisted formal proof generation, suggesting a promising direction for future research in formal mathematical proof.

Figures

Figures reproduced from arXiv: 2502.03321 by the authors.

Figure 1
Figure 1. Examples considering numbers of attempts taken by dChatLean+ Moreover, we observe that, for the problems with successful proofs, the av￾erage number of attempts taken with dChatLean is 10.3, while just 9.3 with [PITH_FULL_IMAGE:figures/full_fig_p013_1.png] view at source ↗
Figure 2
Figure 2. The process of generating a proof for “mathd algebra 171” using the Bad(O)- based feedback algorithm. The highlighted lines indicate the trials selected to be further illustrated in [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Selected proof trials highlighted in blue, also displayed in [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The proof generated by bChatLean for Bernoulli’s inequality using mathematical induction. However, the model uses the pre-defined theorem one add mul le pow, which corresponds to Bernoulli’s inequality in the math￾lib library. While the problem was technically solved, …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 20 canonical work pages

  1. [1]

    Eprint: arXiv:2303.08774

    Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F.L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al.: GPT-4 technical report (2023). Eprint: arXiv:2303.08774

    arXiv 2023

  2. [2]

    Eprint: arXiv:2302.12433

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

    arXiv 2023

  3. [3]

    Eprint: arXiv:2310.10631

    Azerbayev, Z., Schoelkopf, H., Paster, K., Santos, M.D., McAleer, S.M., Jiang, A.Q., Deng, J., Biderman, S., Welleck, S.: Llemma: An open language model for mathematics (2023). Eprint: arXiv:2310.10631

    arXiv 2023

  4. [4]

    In: Conference on Neural Information Processing Systems, vol

    Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J.D., Dhariwal, P., Nee- lakantan, A., Shyam, P., Sastry, G., Askell, A., et al.: Language models are few-shot learners. In: Conference on Neural Information Processing Systems, vol. 33, pp. 1877–1901 (2020). URL https://proceedings.neurips.cc/paper files/paper/2020/ file/1457c0d6bfcb4967418bfb8ac142f64...

    work page 2020

  5. [5]

    Eprint: arXiv:2107.03374

    Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H.P.d.O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al.: Evaluating large language models trained on code (2021). Eprint: arXiv:2107.03374

    arXiv 2021

  6. [6]

    Journal of Machine Learning Research 24(240), 1–113 (2023)

    Chowdhery, A., Narang, S., Devlin, J., Bosma, M., Mishra, G., Roberts, A., Barham, P., Chung, H.W., Sutton, C., Gehrmann, S., et al.: PaLM: Scaling lan- guage modeling with pathways. Journal of Machine Learning Research 24(240), 1–113 (2023). URL http://jmlr.org/papers/v24/22-1144.pdf

    work page 2023

  7. [7]

    Nature 600, 70–74 (2021)

    Davies, A., Veliˇ ckovi´ c, P., Buesing, L., Blackwell, S., Zheng, D., Tomaˇ sev, N., Tanburn, R., Battaglia, P., Blundell, C., Juh´ asz, A., Lackenby, M., Williamson, G., Hassabis, D., Kohli, P.: Advancing mathematics by guiding human intuition with AI. Nature 600, 70–74 (2021). DOI 10.1038/s41586-021-04086-x. URL https://doi.org/10.1038/s41586-021-04086-x

    doi:10.1038/s41586-021-04086-x 2021

  8. [8]

    Communications of the ACM 22(5), 271–280 (1979) 18 S

    DeMillo, R., Lipton, R., Perlis, A.: Social processes and proofs of theorems and programs. Communications of the ACM 22(5), 271–280 (1979) 18 S. Han et al

    work page 1979

Show all 33 references
  1. [9]

    CoRR, abs/2112.15594 (2021)

    Drori, I., Tran, S., Wang, R., Cheng, N., Liu, K., Tang, L., Ke, E., Singh, N., Patti, T.L., Lynch, J., et al.: A neural network solves and generates mathematics problems by program synthesis: Calculus, differential equations, linear algebra, and more. CoRR, abs/2112.15594 (2021)

    2021 arXiv

  2. [10]

    Eprint: arXiv:2309.17452

    Gou, Z., Shao, Z., Gong, Y., Yang, Y., Huang, M., Duan, N., Chen, W., et al.: ToRA: A tool-integrated reasoning agent for mathematical problem solving (2023). Eprint: arXiv:2309.17452

    2023 arXiv

  3. [11]

    In: International Conference on Learning Representations (2022)

    Han, J.M., Rute, J., Wu, Y., Ayers, E.W., Polu, S.: Proof artifact co-training for theorem proving with language models. In: International Conference on Learning Representations (2022)

    2022

  4. [12]

    In: Conference on Neural Information Processing Systems (2021)

    Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., Steinhardt, J.: Measuring mathematical problem solving with the MATH dataset. In: Conference on Neural Information Processing Systems (2021). URL https://datasets-benchmarks-proceedings.neurips....

    2021

  5. [13]

    Communications of the ACM 12(10), 576–580 (1969)

    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969). DOI 10.1145/363235.363259. URL https: //doi.org/10.1145/363235.363259

    1969

  6. [14]

    In: Conference on Neural Information Processing Sys- tems, vol

    Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzyg´ o´ zd´ z, T., Mi l o´ s, P., Wu, Y., Jamnik, M.: Thor: Wielding hammers to integrate language models and automated theorem provers. In: Conference on Neural Information Processing Sys- tems, vol. 35, pp. 8360–8373 (2...

    2022

  7. [15]

    In: International Conference on Learning Representations (2023)

    Jiang, A.Q., Welleck, S., Zhou, J.P., Lacroix, T., Liu, J., Li, W., Jamnik, M., Lample, G., Wu, Y.: Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In: International Conference on Learning Representations (2023)

    2023

  8. [16]

    In: Conference on Neural Information Processing Systems, vol

    Lample, G., Lacroix, T., Lachaux, M.A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., Martinet, X.: Hypertree proof search for neural theorem proving. In: Conference on Neural Information Processing Systems, vol. 35, pp. 26,337– 26,349 (2022). URL https://proceedings.neurip...

    2022

  9. [17]

    In: International Conference on Certified Programs and Proofs, p

    Limperg, J., From, A.H.: Aesop: White-box best-first proof search for Lean. In: International Conference on Certified Programs and Proofs, p. 253–266 (2023). DOI 10.1145/3573105.3575671. URL https://doi.org/10.1145/3573105.3575671

    2023

  10. [18]

    Communications of the ACM 3(4), 184–195 (1960)

    McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM 3(4), 184–195 (1960)

    1960

  11. [19]

    Eprint: arXiv:1505.04324

    de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory (2015). Eprint: arXiv:1505.04324

    2015 arXiv

  12. [20]

    In: International Conference on Learning Representations (2023)

    Polu, S., Han, J.M., Zheng, K., Baksys, M., Babuschkin, I., Sutskever, I.: For- mal mathematics statement curriculum learning. In: International Conference on Learning Representations (2023)

    2023

  13. [21]

    Eprint: arXiv:2009.03393

    Polu, S., Sutskever, I.: Generative language modeling for automated theorem prov- ing (2020). Eprint: arXiv:2009.03393

    2020 arXiv

  14. [22]

    https://xenaproject.wordpress.com/2020/ 12/05/liquid-tensor-experiment/ (2020)

    Scholze, P.: Liquid tensor experiment. https://xenaproject.wordpress.com/2020/ 12/05/liquid-tensor-experiment/ (2020). Last accessed: January 23, 2024

    2020

  15. [23]

    Eprint: arXiv:2310.04353v3

    Thakur, A., Wen, Y., Chaudhuri, S.: A language-agent approach to formal theorem- proving (2023). Eprint: arXiv:2310.04353v3

    2023 arXiv

  16. [24]

    Eprint: arXiv:2302.13971 Simplifying Proof Generation with ChatGPT and Basic Search 19

    Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.A., Lacroix, T., Rozi` ere, B., Goyal, N., Hambro, E., Azhar, F., et al.: LLaMA: Open and efficient foundation language models (2023). Eprint: arXiv:2302.13971 Simplifying Proof Generation with ChatGPT and Basic Search 19

    2023 arXiv

  17. [25]

    Nature 625, 476–482 (2024)

    Trinh, T.H., Wu, Y., Le, Q.V., He, H., Luong, T.: Solving olympiad geometry with- out human demonstrations. Nature 625, 476–482 (2024). DOI 10.1038/s41586- 023-06747-5. URL https://doi.org/10.1038/s41586-023-06747-5

    2024 doi

  18. [26]

    URL https://openreview.net/pdf?id=lxlMFlzZO9

    Vishwakarma, R., Mishra, S.: DS-Prover: A dynamic sampling based approach for neural theorem proving (2024). URL https://openreview.net/pdf?id=lxlMFlzZO9

    2024

  19. [27]

    Eprint: arXiv:2310.00656

    Wang, H., Xin, H., Zheng, C., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., Yin, J., Li, Z., Liang, X.: LEGO-Prover: Neural theorem proving with growing libraries (2023). Eprint: arXiv:2310.00656

    2023 arXiv

  20. [28]

    In: Conference on Neural Information Processing Systems (2021)

    Welleck, S., Liu, J., Han, J.M., Choi, Y.: Towards grounded natural language proof generation. In: Conference on Neural Information Processing Systems (2021)

    2021

  21. [29]

    In: Con- ference on Neural Information Processing Systems, vol

    Wu, M., Norrish, M., Walder, C., Dezfouli, A.: TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. In: Con- ference on Neural Information Processing Systems, vol. 34, pp. 9330– 9342 (2021). URL https://proceedings.neurips.cc/paper files/paper/...

    2021

  22. [30]

    Eprint: arXiv:2408.08152

    Xin, H., Ren, Z.Z., Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., Du, Q., Gao, W., Zhu, Q., Yang, D., Gou, Z., Wu, Z.F., Luo, F., Ruan, C.: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (2...

    2024 arXiv

  23. [31]

    In: International Conference on Machine Learning, vol

    Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assis- tants. In: International Conference on Machine Learning, vol. 97, pp. 6984–6994 (2019). URL http://proceedings.mlr.press/v97/yang19a/yang19a.pdf

    2019

  24. [32]

    In: Conference on Neural Information Processing Systems (2023)

    Yang, K., Swope, A.M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., Anandkumar, A.: LeanDojo: Theorem proving with retrieval-augmented lan- guage models. In: Conference on Neural Information Processing Systems (2023)

    2023

  25. [33]

    In: International Conference on Learning Represen- tations (2022)

    Zheng, K., Han, J.M., Polu, S.: MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. In: International Conference on Learning Represen- tations (2022)

    2022

Pith tools

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