Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving

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

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

Pith's one-line read One neural prover trained on both Lean and Coq tactic data beats single-language provers in proof search.

desk verdict Solid infrastructure paper with a real but over-claimed cross-lingual transfer result; needs an equal-size control before the headline claim holds. read the letter →

arxiv 2502.04671 v3 pith:OKDR57N5 submitted 2025-02-07 cs.AI cs.LGcs.LOcs.PL

Amitayush Thakur , George Tsoukalas , Greg Durrett , Swarat Chaudhuri This is my paper · ORCID
classification cs.AIcs.LGcs.LOcs.PL MSC 03B3568T07
keywords theoremprovinginteractiveproversLean4Coqmultilingualtrainingproof-stepdatabeamsearchtransferlearning
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 neural theorem prover trained on proof-step data from two different proof assistants, Lean 4 and Coq, becomes better at proving theorems in either language than a model trained on only one. The authors build ProofWala, a framework that extracts standardized tactic-by-tactic proof data from both systems, trains a single tactic-prediction model on any mix of that data, and wraps it in parallel beam search. In their experiments, the mixed-language model outperforms the Lean-only and Coq-only models on prove-at-k (the fraction of theorems proved within $k$ sampled proof attempts) across all five evaluated data mixes at $k=5$, with statistically significant gains on the largest Lean benchmark and on a category-theory library after further fine-tuning. The significance is that cross-lingual transfer could let formal proof data collected in one assistant improve proving in another, easing the data bottleneck in neural theorem proving.

What carries the argument

The load-bearing object is the standardized proof-step record: for each tactic application, the triple of pre-state, tactic, and post-state, serialized in one JSON format for both Lean and Coq, and turned into a training prompt that deliberately omits any clue about which assistant or domain produced the state. That uniformity makes the problem look the same across languages to one 220-million-parameter code model. Around this record, ProofWala provides an interaction layer (Lean 4 tactics are traced meta-programmatically inside the elaborator; Coq interaction reuses an existing serialization backend), a pool of parallel proof-environment workers that lets many candidate tactics be executed simultaneously on cloned states, and beam search guided by the model's token log-likelihoods.

What would settle it

Rerun the prove-at-k comparison under a leakage-controlled split: cluster test theorems by statement similarity or dependency overlap with training theorems, keep only the clusters with no near-duplicate in training, and see whether the multilingual advantage persists. A second concrete check is to add the assistant's name back into the training prompt; if the gap between the multilingual and monolingual models disappears, the transfer is an artifact of hiding the source language.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that multilingual training across Lean 4 and Coq produces positive cross-lingual and cross-domain transfer for proof-step prediction. A model fine-tuned on a mix of Coq and Lean data (the multilingual model) matches or beats the corresponding monolingual models on all five benchmark suites: at pass@5 it is best on every suite, and the edge is statistically significant ($p<0.05$ by paired bootstrap) on the largest Lean benchmark and, after additional fine-tuning, on an out-of-domain category-theory suite. The paper also reports that the multilingual model builds larger proof trees during search, finding more compilable tactics per proof state, and that it sometimes finds multiple proofs for the same theorem. These results are offered as evidence that shared training across assistants generalizes better than training within a single assistant.

Load-bearing premise

The transfer result rests on the assumption that the random train/test splits for the three smaller Coq-derived suites do not leak near-duplicate theorems into training; if that assumption fails, the reported gains would reflect memorization rather than cross-lingual transfer.

Editorial extensions

If this is right

  • A single proof-step model can serve as a usable prover in both Lean 4 and Coq, so new repositories do not need assistant-specific training pipelines.
  • Starting from multilingual pretraining improves adaptation to a new domain compared to starting from a monolingual model, which is evidence for the authors' claim that such models should be preferred as completion assistants for newly developing formal repositories.
  • Parallel execution of candidate tactics on cloned proof states makes wider beam search practical, so search can cover more of the proof space within a fixed wall-clock timeout.
  • The released framework, datasets, and models let other groups reproduce or extend the multilingual-training recipe without rebuilding the interaction infrastructure.

Reading between the lines

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

  • If hiding the assistant's identity is the active ingredient, then adding the assistant name back to the prompt should shrink the transfer gain; this is directly testable as an ablation.
  • Should the transfer scale with data, the same standardized pipeline could be extended to other tactic-based proof assistants, with larger gains expected from assistants that share tactic families with Lean or Coq.
  • The larger proof trees observed for the multilingual model may reflect a broader actionable tactic vocabulary rather than better prioritization; comparing proofs found under a fixed node budget, rather than a fixed timeout, would separate these two explanations.
  • Because the random train/test splits do not control for theorem similarity, a stricter family-based split is needed to rule out memorization as the source of the reported improvement.
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 / 5 minor

Summary. The paper presents ProofWala, an open-source framework for extracting proof-step data from Lean 4 and Coq/Rocq repositories, training proof-step prediction models, and running parallel proof search. The authors construct datasets from CompCert, Mathlib, MathComp, GeoCoq, and CategoryTheory; fine-tune CodeT5-base on monolingual and multilingual mixes; and evaluate prove-at-k performance on held-out theorems. Their central empirical claim is that a model trained on combined Lean+Coq data outperforms models trained on either language alone, with statistically significant gains on Mathlib and CategoryTheory and consistent upward trends elsewhere.

Significance. The framework is a solid engineering contribution: it unifies ITP interaction, standardizes the data format, supports repository-scale extraction, and ships open-source code, data, and models. The evaluation uses machine-checked tactic execution in the ITPs and paired bootstrap tests, which are appropriate tools. If the cross-lingual transfer claim were cleanly established, it would matter for data-scarce settings in neural theorem proving. However, the current experiments do not isolate the multilingual mechanism from the effect of additional training data, so the significance of the headline result is currently limited.

major comments (3)
  1. [§4.1–4.2, Table 3] The comparison between PROOFWALA-MULTILINGUAL and the monolingual baselines confounds cross-lingual training with corpus size: the multilingual model trains on 442,607 proof-step pairs (270M tokens), while PROOFWALA-LEAN uses 237,003 pairs (99M tokens) and PROOFWALA-COQ uses 205,604 pairs (171M tokens). Because the multilingual model sees all of the target language data plus a large auxiliary corpus, its higher pass@5 scores could reflect generic benefits of a larger, more diverse training set rather than transfer between Lean and Coq. Training all models for the same number of gradient updates (Appendix A.3) does not remove this confound, since each update consumes a different, larger data distribution. An equal-size control—for example, a Lean-only model trained on Lean data plus a same-language corpus matched to the multilingual token count, or a model trained on target data plus randomly relabeled other-language data—is needed to attribute the gains to cross-lingual transfer.
  2. [§5.1, Table 3 and caption] The text states that transfer occurs 'on all data-mixes,' but at pass@1 the multilingual model is worse than the COQ model on MathComp (27.9 vs 28.28) and GeoCoq (30.89 vs 32.87), and the advantage appears only at higher k. Moreover, the paired bootstrap tests are significant only for LEAN (p=0.018) and CategoryTheory (p=0.008); the other p-values (0.355, 0.135, 0.191) are not. The abstract should specify pass@5 when claiming superiority on the prove-at-k metric, and the body should avoid the 'all data-mixes' phrasing.
  3. [§5.1, CategoryTheory experiment] The further-fine-tuning experiment is the cleanest comparison because both models are fine-tuned on the same 1.7M-token CategoryTheory split, and the 8-point gain at pass@1 (44.55 vs 36.63) is encouraging. However, it is based on only 101 test theorems, and the two base models still differ in pretraining corpus size and composition. This experiment should be presented as preliminary evidence that multilingual pretraining helps domain adaptation, not as a conclusive demonstration of a multilingual-specific effect.
minor comments (5)
  1. [§5.1] Define pass@k precisely for the beam-search setup; the citation to Chen et al. (2021) is not sufficient because beam width 32 and a timeout do not map directly to the standard sampling-based definition of pass@k.
  2. [§4.1] Clarify the unit of the 'randomly decided' split; specify that it is at the theorem level and that no theorem appears in both train and test splits, since the current phrasing is ambiguous.
  3. [§5.1] The unsupported statement that PROOFWALA-MULTILINGUAL outperforms Proverbot on CompCert should be either substantiated with the Proverbot result or removed.
  4. [§5.1, Table 7] The proof-tree statistics (more nodes, edges, and degree) are descriptive; note that the multilingual model takes longer on most datasets and that larger trees do not by themselves indicate more effective search.
  5. [Throughout] Fix inconsistent spacing of 'ProofWala' (e.g., 'P ROOF WALA') and complete the sentence in Section 3's header, which currently reads 'in alanguage-agnostic manner' instead of 'in a language-agnostic manner'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the multilingual transfer claim is an empirical search outcome, not a construction-fitted or self-citation-forced result.

full rationale

The paper's central claim is that a model trained on mixed Lean and Coq proof-step data improves proof search, and this is evaluated by held-out pass@k experiments (Table 3) using external repository splits. The pass@k numbers are produced by beam search over ITP-checked proof steps, not by any equation that defines the result in terms of the training data. The only self-references are infrastructural: the prompt format is said to be inspired by the authors' earlier COPRA framework, and the search formulation follows their earlier work on theorem-proving as discrete search. Neither of these is load-bearing for the multilingual-transfer conclusion, and neither imports an unverified uniqueness or forcing result. The model is fine-tuned on training splits and evaluated on test theorems; no fitted parameter is renamed as a prediction, and no theorem-level conclusion is equivalent to its own input by construction. The skeptic's concern about corpus-size confounding and random-split leakage is a validity or experimental-design issue about whether the observed gains are caused by cross-lingual transfer, not a circularity in the derivation. Since the paper's evidence is self-contained against held-out proof search, the appropriate finding is no significant circularity.

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

This is an empirical systems paper; the central claims rest on the soundness of ITP interactions, the fairness of data splits, and the adequacy of the chosen model backbone, not on new mathematical postulates or invented entities.

free parameters (5)
  • Number of training steps = 34000
    All models trained for 34000 gradient updates to equalize compute; this choice follows Jiang et al. (2023) and bounds the training budget.
  • Batch size = 128
    Used for all primary models; influences the number of examples per update.
  • Beam width = 32
    Beam search width in the proof search module; fixed across all evaluations.
  • Sampling temperature = 0.75
    Temperature for sampling proof steps during beam search.
  • Search timeout = 600 seconds (1200 for GeoCoq)
    Timeout per proof attempt; affects pass@k and proof-tree sizes.
assumptions (3)
  • domain assumption Lean 4 and Coq tactic execution correctly reflects the formal semantics of proofs
    The entire training data and evaluation depend on the ITP checkers being sound; the paper notes it fixed a REPL bug that accepted incorrect proofs (Appendix A.5).
  • domain assumption Random train/test splits for MathComp, GeoCoq, and CategoryTheory do not create theorem-level leakage
    Section 4.1 states splits are randomly decided; the transfer claim depends on test theorems being unseen.
  • domain assumption CodeT5-base is an adequate backbone for cross-lingual proof-step prediction
    The choice of CodeT5-base is empirical; no guarantee that results transfer to other architectures.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving." pith.science (2026). https://pith.science/paper/OKDR57N5

@misc{pith2026250204671,
  author       = {Pith},
  title        = {Pith review of: ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OKDR57N5}},
  note         = {Machine review of arXiv:2502.04671}
}
read the original abstract

Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof search at scale. However, existing tooling is often assistant-specific and oriented toward file-level execution, making repository-scale analysis and parallel experimentation challenging. We present ProofWala, a multilingual proof engineering framework built around \texttt{itp-interface}, a reusable library for programmatic interaction with ITPs. For Lean 4, we implement a meta-programmed interaction layer executing inside the elaborator, enabling semantically faithful tactic-level tracing alongside declaration- and dependency-level extraction across entire repositories. This design extends beyond traditional REPL-style interaction by supporting project-wide analysis, environment cloning, and pooled execution of proof states. The same interface abstraction supports multiple versions of Rocq, yielding a unified cross-assistant pipeline. Built on this infrastructure, ProofWala provides standardized multilingual proof datasets, model training utilities, and parallel proof search algorithms. Using the framework, we demonstrate that multilingual training across Lean and Rocq enables cross-lingual and cross-domain transfer. We observe statistically significant improvements on Lean Mathlib and in domain adaptation (CategoryTheory), while other settings exhibit consistent upward trends. We open-source the full framework, parallel proof search module, datasets, and models across two repositories: ProofWala (https://github.com/trishullab/proof-wala) and the itp-interface library (https://github.com/trishullab/itp-interface).

Figures

Figures reproduced from arXiv: 2502.04671 by the authors.

Figure 1
Figure 1. shows a formal proof of a theorem about block triangular matrices —found using the PROOFWALA￾theorem blockTriangular_stdBasisMatrix {i j : m} (hij : b i ≤ b j) (c : R) : BlockTriangular (stdBasisMatrix i j c) b := by rintro i' j' hij' simp [stdBasisMatrix, hij, hij'.not_le] rintro rfl rfl exact (not_lt_of_le hij hij').elim [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The PROOFWALA Framework with the interaction between different modules. Using PROOFWALA’s interaction & data-collection modules, we collect a multilingual proof dataset from existing formal mathematics repositories in LEAN and COQ. The resulting dataset is used to train a multilingual proof step prediction model, supported by PROOFWALA’s training module. The multilingual model is used inside PROOFWALA’s search modul… view at source ↗
Figure 3
Figure 3. Distribution of degree of nodes in the proof trees across various data mixes found by different [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: An excerpt from the extracted training data sequence, [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]
Figure 5
Figure 5. Figure 5: Prompt format for training the proof step generation model. (a) shows the prompt format for [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]
Figure 6
Figure 6. Figure 6: Pseudocode for the parallel proof search module utilizing Beam Search with the Ray framework ( [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Visualization of the proof trees generated via the [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 8
Figure 8. Figure 8: Distribution of proof-tree nodes across various data-mixes found by different [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: Distribution of proof-tree edges across various data-mixes found by different [PITH_FULL_IMAGE:figures/full_fig_p016_9.png]
Figure 10
Figure 10. Figure 10: Distribution of the number of proofs found for the same theorem across various data-mixes found by different [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: Distribution of the time taken to find proofs across various data-mixes found by different [PITH_FULL_IMAGE:figures/full_fig_p017_11.png]
Figure 12
Figure 12. Figure 12: Some proofs discovered by PROOFWALA-MULTILINGUAL in our experiments on theorems from Mathlib, GeoCoq, and MathComp. 17 [PITH_FULL_IMAGE:figures/full_fig_p017_12.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities

    cs.LO 2026-06 unverdicted novelty 7.0 of 10

    AXLE is a multi-tenant cloud platform providing Lean 4 metaprogramming utilities with per-request isolation, multi-version support, and public access via SDK and API, having processed over 500 million requests.

Reference graph

Works this paper leans on

34 extracted references · 17 canonical work pages · cited by 1 Pith paper

  1. [1]

    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 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

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

    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, 2024. URL https://arxiv.org/abs/2410.16429

    arXiv 2024

  3. [3]

    The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq, pp.\ 271–277

    Blaauwbroek, L., Urban, J., and Geuvers, H. The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq, pp.\ 271–277. Springer International Publishing, 2020. ISBN 9783030535186. doi:10.1007/978-3-030-53518-6_17. URL http://dx.doi.org/10.1007/978-3-030-53518-6_17

    doi:10.1007/978-3-030-53518-6_17 2020

  4. [4]

    Blaauwbroek, L., Olšák, M., Rute, J., Massolo, F. I. S., Piepenbrock, J., and Pestun, V. Graph2tac: Online representation learning of formal math concepts, 2024. URL https://arxiv.org/abs/2401.02949

    work page Pith review arXiv 2024

  5. [5]

    F., and First, E

    Carrott, P., Saavedra, N., Thompson, K., Lerner, S., Ferreira, J. F., and First, E. Coqpyt: Proof navigation in python in the era of llms. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, volume 21612 of FSE ’24, pp.\ 637–641. ACM, July 2024. doi:10.1145/3663529.3663814. URL http://dx.doi.org/10...

    work page arXiv 2024

  6. [6]

    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. arXiv preprint arXiv:2107.03374, 2021

    arXiv 2021

  7. [7]

    The Lean theorem prover (system description)

    de Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp.\ 378--388. Springer, 2015

    work page 2015

  8. [8]

    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. URL https://openreview.net/forum?id=kk3mSjVCUO

    work page 2024

Show all 34 references
  1. [9]

    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

  2. [10]

    The coq proof assistant a tutorial

    Huet, G., Kahn, G., and Paulin-Mohring, C. The coq proof assistant a tutorial. Rapport Technique, 178, 1997

    1997

  3. [11]

    Q., Li, W., and Jamnik, M

    Jiang, A. Q., Li, W., and Jamnik, M. Multilingual mathematical autoformalization, 2023. URL https://arxiv.org/abs/2311.03755

    2023 arXiv

  4. [12]

    Coqpilot, a plugin for llm-based generation of proofs

    Kozyrev, A., Solovev, G., Khramov, N., and Podkopaev, A. Coqpilot, a plugin for llm-based generation of proofs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE ’24, pp.\ 2382–2385. ACM, October 2024. doi:10.1145/3691620.36953...

    2024

  5. [13]

    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

  6. [14]

    Formal verification of a realistic compiler

    Leroy, X. Formal verification of a realistic compiler. Communications of the ACM, 52 0 (7): 0 107--115, 2009

    2009

  7. [15]

    A survey on deep learning for theorem proving, 2024

    Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., and Si, X. A survey on deep learning for theorem proving, 2024. URL https://arxiv.org/abs/2404.09939

    2024 arXiv

  8. [16]

    G it H ub - math-comp/math-comp: M athematical C omponents --- github.com

    Mathcomp. G it H ub - math-comp/math-comp: M athematical C omponents --- github.com. https://github.com/math-comp/math-comp, 2015. [Accessed 01-06-2024]

    2015

  9. [17]

    The lean mathematical library

    mathlib Community, T. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. doi:10.1145/3372885.3373824. URL http://dx.doi.org/10.1145/3372885.3373824

    2020

  10. [18]

    I., et al

    Moritz, P., Nishihara, R., Wang, S., Tumanov, A., Liaw, R., Liang, E., Elibol, M., Yang, Z., Paul, W., Jordan, M. I., et al. Ray: A distributed framework for emerging \ AI \ applications. In 13th USENIX symposium on operating systems design and implementation (OSDI 18), pp.\ 5...

    2018

  11. [19]

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

    1994

  12. [20]

    and Sutskever, I

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

    2009 arXiv

  13. [21]

    Generating correctness proofs with neural networks

    Sanchez-Stern, A., Alhessi, Y., Saul, L., and Lerner, S. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pp.\ 1--10, 2020

    2020

  14. [22]

    Towards large language models as copilots for theorem proving in lean, 2024

    Song, P., Yang, K., and Anandkumar, A. Towards large language models as copilots for theorem proving in lean, 2024. URL https://arxiv.org/abs/2404.12534

    2024 arXiv

  15. [23]

    An in-context learning agent for formal theorem-proving

    Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaudhuri, S. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling, 2024

    2024

  16. [24]

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

    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, 2024. URL https://arxiv.org/abs/2407.11214

    2024 arXiv

  17. [25]

    Wang, Y., Wang, W., Joty, S., and Hoi, S. C. Codet5: Identifier-aware unified pre-trained encoder-decoder models for code understanding and generation. In EMNLP, 2021

    2021

  18. [26]

    and Saha, R

    Welleck, S. and Saha, R. Llmstep: Llm proofstep suggestions in lean, 2023. URL https://arxiv.org/abs/2310.18457

    2023 arXiv

  19. [27]

    and Deng, J

    Yang, K. and Deng, J. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp.\ 6984--6994. PMLR, 2019

    2019

  20. [28]

    M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A

    Yang, K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626, 2023

    2023 arXiv

  21. [29]

    Formal mathematical reasoning: A new frontier in ai, 2024

    Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A new frontier in ai, 2024. URL https://arxiv.org/abs/2412.16075

    2024 arXiv

  22. [30]

    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

  23. [31]

    Neural theorem proving toolkit, 2023

    Zhu, T., Clune, J., and Welleck, S. Neural theorem proving toolkit, 2023. URL https://github.com/cmu-l3/ntp-toolkit

    2023

  24. [32]

    @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 ...

  25. [33]

    \@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...

  26. [34]

    output.w18

    @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 8, 2026 · model on record in the stance chip above.