Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

Kevin Han; Kevin Zhu; Tim Knappe; Vincent Li; Yule Fu

REVIEW 5 major objections 6 minor 25 references

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

T0 review · 5 major / 6 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 KG-Prover claims that injecting a knowledge graph mined from a curated mathematics compendium into off-the-shelf LLMs, and scaling traversal depth with best-of-N and beam search, raises theorem-proving accuracy by up to 21% on…

desk verdict Plausible retrieval-helps result, but the graph-scaling attribution is not established without a compute-matched control. read the letter →

arxiv 2503.11657 v3 pith:22BR25DU submitted 2025-02-04 cs.CL

Vincent Li , Tim Knappe , Yule Fu , Kevin Han , Kevin Zhu This is my paper · ORCID

classification cs.CL

keywords automatedtheoremprovingknowledgegraphtest-timecomputescalingretrieval-augmentedgenerationnaturallanguageproofsLean4verificationbeamsearchbest-of-Nsampling

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

KG-Prover tries to establish that a general-purpose LLM can prove more theorems in natural language when, at inference time, it is given semantically retrieved and graph-expanded context from a large mathematical knowledge graph. The paper claims accuracy gains of up to 21% on miniF2F-test, consistent 2-11% improvements across ProofNet, miniF2F-test, and MUSTARDSAUCE, and further gains from scaling test-time compute via traversal depth, best-of-N sampling, and beam search. If true, this matters because it would mean substantial theorem-proving progress is available without finetuning on formal corpora: an off-the-shelf model, a curated concept graph, and a Lean verification loop may suffice. The framework separates proof generation from formalization, so the natural-language reasoning is judged by Lean rather than assumed correct.

What carries the argument

The central object is the proof-knowledge graph $G=(V,E)$ built from a curated mathematics compendium, where each node is a definition, theorem, lemma, or corollary and hyperlinks between pages become edges. Given a proposition $P$, the system embeds $P$ and scores all nodes by cosine similarity $S=\frac{v_P\cdot v_i}{\lVert v_P\rVert_2\lVert v_i\rVert_2}$, uses the top-$k$ nodes as initial context, and if the proof fails Lean verification, expands to the top-$k$ 1-hop neighbors of already traversed nodes up to a depth $D$ with $r$ attempts. A judge-based best-of-$N$ selection and beam-search refinement scale the candidate generation at test time, and a separate autoformalizer translates the winning informal proof into Lean 4 for verification.

What would settle it

Run a compute-matched control that spends the same 30 LLM calls per problem on best-of-N sampling or repeated chain-of-thought retries with no graph context; if that control matches or beats KG-Prover's 31.97% on miniF2F-test, the claim that the graph drives the gains would be refuted.

Watch

Extended reading notes

Core claim

On the paper's own terms, KG-Prover discovers that injecting related mathematical statements retrieved from a ProofWiki-derived knowledge graph into the prompt of a general-purpose LLM, and iteratively expanding retrieval to neighboring nodes when Lean verification fails, reliably improves proof success rates across benchmarks. The headline results are a rise from 20.49% to 31.97% for Llama 3.1 8B on miniF2F-test and 52.9% for o4-mini with beam search, with consistent gains on ProofNet and MUSTARDSAUCE. The authors present this as evidence that graph-structured knowledge, rather than additional training, can supply the missing concepts and dependencies that LLMs need for formal mathematical proof.

Load-bearing premise

The load-bearing premise is that the accuracy gains come from the knowledge graph's structure and traversal, not from the extra test-time compute or a weak retrieval baseline, because KG-Prover is allowed up to 30 LLM calls per problem while the RAG baseline uses a fixed context with only retries.

Editorial extensions

If this is right

Any general-purpose LLM in the study improves on at least one of the three benchmarks when graph context is added, with the largest jump on miniF2F-test.
Scaling traversal depth, candidate count, and beam width keeps improving accuracy, with the first three depth steps delivering most of the gain.
Finetuned Lean provers also gain from the graph: TheoremLlama's pass@128 rises from 35.04% to 36.89% when KG-Prover context is included.
Because retrieval, informal proof generation, autoformalization, and verification are separate stages, each can be replaced or upgraded independently in future systems.

Reading between the lines

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

The paper leaves implicit that the same traversal-retrieval design could serve other multi-step reasoning tasks where a concept graph exists, turning verifier feedback into a retrieval signal.
A testable extension is to substitute domain-specific concept graphs, such as physics or chemistry formalisms, and check whether the same depth-scaling curve appears; that would show the mechanism is graph structure rather than mathematics-specific content.
Their failure analysis reports about 35% of failures come from translating a largely correct informal proof into Lean, which suggests the next bottleneck may be autoformalization quality rather than retrieval coverage.
An ablation that fixes the LLM-call budget across methods would clarify how much of the reported gain is due to graph structure versus simply more attempts and more context.

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.

Desk Editor's Note

read the letter

Quick take: this is a modest, believable idea with a real verification setup, but the headline claim about graph-based scaling is not supported by the experiments as reported.

The genuinely new piece is the specific pipeline: a ProofWiki-derived knowledge graph, embedding-based retrieval, iterative neighbor expansion, an LLM judge for best-of-N and beam search, and informal-to-Lean verification. The graph itself (60k nodes, 300k edges) is a useful asset. Because correctness is checked by the external Lean verifier on public benchmarks, the successes in Tables 1 and 5 are real proofs, not self-assessed. The general direction that retrieved context helps LLM theorem proving is consistent with prior RAG work and the table-level trends are consistent across six models.

The soft spots are central, not cosmetic. Table 1's caption says KG-Prover "may additionally apply beam search" while Base and RAG generate a single completion per Lean retry. Table 3 shows that beam configuration uses 30 LLM calls per problem versus 3 for baselines. There is no compute-matched control, such as best-of-N sampling over a flat retrieval corpus with the same call and token budget. Figure 3's x-axis is labeled "Traversal Depth r" but Section 5.3 defines r as consecutive attempts, so the scaling curves are equally explained by "more retries help" without any graph. The semantic search description in Appendix H.2 ("avoids exhaustive traversal") makes it unclear whether graph edges are used at all in the reported system. There are also no error bars or significance tests, hyperparameters appear to be chosen on the test set, the abstract's "up to 21%" does not match Table 1, the traversal equation in Section 3.2.1 is garbled, and no GitHub link appears despite the reproducibility statement.

None of this kills the underlying idea. A revision with a compute-matched baseline, error bars, and a clean graph-versus-retries ablation would tell us whether the graph structure earns its complexity. As written, the quantitative claims run ahead of the evidence.

This paper is for researchers working on retrieval-augmented theorem proving or test-time compute scaling. They would get value from the system description and the failure analysis, but should not take the headline numbers at face value. It deserves a serious referee because the question is real and the verification setup is sound, but I would expect major revision before it is citable.

Referee Report

5 major / 6 minor

Summary. The paper introduces KG-Prover, a training-free framework that augments general-purpose LLMs with a knowledge graph mined from ProofWiki for automated theorem proving. At inference time, KG-Prover embeds the problem statement, retrieves semantically similar nodes, generates an informal proof, autoformalizes it with DeepSeek-Prover-V1.5, and verifies it in Lean. If verification fails, the system traverses the graph to add neighboring nodes and retries, optionally using best-of-N selection or beam search. The authors evaluate on miniF2F, ProofNet, and MUSTARDSAUCE with six LLMs, and report consistent improvements over zero-shot baselines and a fixed top-5 RAG baseline, with the largest gains on miniF2F (e.g., Llama 3.1 8B at 31.97% vs. 20.49% baseline) and 52.9% for o4-mini with beam search. The central claim is that graph-based retrieval and traversal, scaled at test time, drive these gains.

Significance. If the central attribution were established, this would be a practically useful result: it shows that retrieval from an open mathematical corpus can improve general-purpose LLM theorem proving without finetuning, and the use of the external Lean verifier plus public benchmarks is a genuine strength. The paper is also transparent about token and API-call costs (Table 3), reports deterministic evaluations, and makes code available. However, the significance is currently limited by the absence of compute-matched controls: the reported gains conflate graph traversal with extra retries and beam search, so the title's claim that graph-based test-time compute is the driver is not yet supported. The framework is plausible and the direction of the effect is consistent with prior retrieval-augmented reasoning results, but the magnitude and attribution need stronger evidence.

major comments (5)

[§5.3, Figure 3, §4.4] The paper conflates graph traversal depth with the number of LLM attempts. Section 5.3 defines r as 'multiple consecutive attempts' for failure correction, while Figure 3 labels its x-axis 'Traversal Depth r'. Under this definition, any point at depth >3 in Figure 3 uses strictly more LLM calls than the Base and RAG baselines (which are fixed at r=3), so the accuracy-vs-depth curves are equally explained by 'more retries help' as by 'deeper graph traversal helps'. The reported scaling claim therefore requires compute-matched controls, e.g., best-of-N sampling from a flat top-k retrieval context with the same number of generations and tokens, and repeated generation at a fixed graph depth without new node injection.
[§4.3, Table 1, Table 3] The comparison in Table 1 is not compute-matched and the caption admits as much: Base and RAG generate a single completion per Lean retry, while 'KG-Prover may additionally apply beam search as detailed in §5.4'. Table 3 shows that the beam configuration uses r[n + w(w^s − 1)/(w − 1)] = 30 LLM calls per problem versus 3 for Base and RAG. Under this protocol the KG-Prover row includes extra test-time compute and search, so headline improvements such as 31.97% vs. 20.49% on miniF2F can be produced by compute alone. The authors should report the exact configuration used for every Table 1 row and include flat-context beam/best-of-N baselines with identical call and token budgets.
[§5.1, Table 1] No uncertainty quantification is provided. ProofNet has 186 problems, miniF2F 244, and MUSTARDSAUCE 250, so several reported differences of 1–2 percentage points (e.g., ProofNet Llama 3.1 8B: 4.30% vs. 3.76%; miniF2F o1-mini: 30.74% vs. 28.28%) are within plausible binomial noise. The paper should report confidence intervals or significance tests (e.g., McNemar or bootstrap) and, for nondeterministic settings, multiple seeds. Without this, the claim of 'consistent improvements ranging from 2–11%' is not warranted.
[§3.2.1, Appendix H.2] There is an internal inconsistency about whether graph edges are used at all. Section 3.2.1 defines traversal over the 1-hop neighbors V_d of the traversed set, but Appendix H.2 describes the semantic-search implementation as 'avoid[ing] exhaustive traversal' and incrementally adding 'the most similar nodes' to the prompt. If the reported rows are actually produced by flat semantic similarity rather than graph adjacency, the paper's central graph-based claim is untested. The authors should clarify which experimental rows use graph edges, and include an ablation that shuffles or randomizes node order within the same retrieved-context set.
[§4.4, §5.2, Figure 2, Table 6] The six free parameters introduced in §4.4 (k, r, d, n, w, search depth) are tuned on the test benchmarks themselves: depth is varied in Figure 2, n is varied in Table 6, and the 'depth = 6' configuration in Table 2 is reported on miniF2F test. No validation-split protocol or fixed default configuration is described. This creates a risk that the reported 'best' numbers are selected from many configurations on the test set. A sensitivity analysis with a fixed default configuration and a hold-out validation protocol is needed before the reported gains can be taken at face value.

minor comments (6)

[§4.3.1] The baseline description says 'single-completion, single-retry budget' but then specifies 'on failure we repeat the same single-completion pipeline up to r=3 times'; the wording should be aligned with the actual r=3 budget.
[§3.2.1] The notation for V_{d-1} is circular: 'V_{d-1} is defined as the set of v_j: ∃(a,b) ∈ E where a ∈ V_{d-1}'. Please define V_0 and the neighbor-expansion step with distinct index names.
[Table 2] The pass@128 comparison is unclear: the table reports TheoremLlama at pass@128 (35.04%) and TheoremLlama + KG-Prover at 36.89%, but the number of proof attempts, tokens, and traversal budget for the KG-Prover row is not stated, so the comparison may not be budget-matched.
[§5.4] The phrase 'on average performs on par better' is grammatically confusing; it should be rewritten to state whether the depth-1 configuration is better or equal to the non-scaling KG-Prover.
[§7] The Limitations section contains an incomplete sentence ending 'different attention mechanisms or.' and the phrase 'disrupt of affect' should be 'disrupt or affect'.
[§8] The reproducibility statement says the code is publicly available on GitHub but provides no URL, repository name, or commit hash; please include a link.

Circularity Check

1 steps flagged · score 6.0 of 10

Traversal-depth scaling curves relabel the retry count r as graph depth, so the headline scaling claim reduces to repeated attempts; the non-scaling graph retrieval results remain externally verified and non-circular.

renaming known result [Section 5.3 (Scaling Traversal Depth) and Figure 3 caption; cf. Section 4.4 parameter definitions and Table 3.]
"To allow the model for failure correction and improvement, the graph system has multiple consecutive attempts defined as r. Each attempt allows the model to traverse further in the graph and explore more nodes."

In Section 4.4 the paper defines r as 'attempts allowed per proof', and Table 3 prices KG-Prover at r(Tp+Tr), i.e., repeated LLM generation calls. Section 5.3 then calls the same r 'traversal depth' and Figure 3 plots 'Accuracy increases with greater traversal depth r', presenting accuracy-vs-retries as evidence of graph-depth scaling. The independent variable is the retry count by the paper's own definition, so the scaling result reduces to the known effect of repeated sampling/self-consistency relabeled as graph traversal. No compute-matched baseline separates the benefit of extra graph nodes from the benefit of extra attempts, so the causal attribution to the graph is asserted by renaming r rather than derived from a graph-depth variable.

full rationale

The paper's non-scaling KG-Prover result is not circular: correctness is adjudicated by the external Lean verifier on public benchmarks (miniF2F, ProofNet, MUSTARDSAUCE), the knowledge graph is built from the external ProofWiki corpus, and no fitted parameter is renamed as a prediction. The LLM judge only ranks candidates before Lean verification, so it does not determine pass/fail. However, the paper's scaling claim for 'traversal depth' is undermined by a definitional conflation: r is defined in Section 4.4 as the number of attempts per proof, Table 3 treats each attempt as a repeated LLM call, and Section 5.3/Figure 3 relabel this retry count as 'traversal depth r'. The plotted scaling behavior is therefore, by the paper's own definition, accuracy versus number of attempts, a known and expected pattern, rather than a demonstrated effect of graph structure. This gives a partial circularity in the central scaling claim, while the independent graph-retrieval comparisons in Table 1 retain genuine external content.

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

The system introduces no new mathematical entities. Its claims rest on several domain assumptions about retrieval, graph structure, and autoformalization reliability, plus a set of hand-chosen hyperparameters that are swept on the test sets. The absence of held-out tuning and error bars makes the quantitative gains fragile.

free parameters (6)

k (top-k nodes per traversal depth) = 5 (default; can be smaller when neighbors are scarce)
Hand-chosen retrieval budget; reported results use top-k=5 and no thorough ablation is shown, yet the composition of the context depends on it.
r (traversal attempts / depth) = 3 default; swept to 7
Headline results depend on this test-time budget; Figure 3 shows accuracy grows with r, so the effect of graph depth is conflated with the number of retries.
n (best-of-N candidates) = 2, 6, 10 in Table 6
Best settings differ by dataset (N=10 for miniF2F, N=2 for ProofNet), suggesting instability and test-set selection.
w (beam width) = 3 (Figure 2)
Doubling to 6 reportedly adds at most 1 percentage point while tripling token usage (Section 5.6).
s (beam search depth) = 2 (Figure 2)
Used in the high-scaling configuration; no separate validation is reported.
Ns (sentence truncation limit) = 4
When the prompt exceeds the 32k context, the first 4 sentences of each snippet are kept and least-similar nodes are dropped (Section 3.2.2).

assumptions (5)

domain assumption ProofWiki hyperlinks encode mathematically meaningful dependency and topic relationships.
Edges are formed from hyperlinks between pages; traversal selects 1-hop neighbors by embedding similarity, so the value of traversal depends on these edges capturing proof-relevant relationships (Section 3.1).
domain assumption Cosine similarity between OpenAI embeddings of mathematical statements correlates with proof relevance.
Used for initial retrieval and neighbor ranking (Section 3.2.1); the authors acknowledge embeddings can lose fine-grained logical structure (Section 7).
domain assumption DeepSeek-Prover-V1.5 can reliably autoformalize informal proofs into verifiable Lean 4 code.
All pass-rate numbers pass through this autoformalizer (Sections 3.2.3 and 4.1); Appendix J reports about 35% of failures are autoformalization failures, so this assumption materially affects measured accuracy.
domain assumption The LLM judge's ranking correlates with proof correctness.
Best-of-N and beam search rely on judge scores (Sections 3.3.1 and 3.3.2); Appendix C shows larger N sometimes hurts, indicating the judge is imperfect.
ad hoc to paper Reported hyperparameter configurations are not overfit to the test sets.
Depth 6, n=5, w=3, s=2, temperature 0.7 and the specific dataset subsets are reported without a held-out validation split (Sections 4.4, 5.4, and Appendix G).

how reviews work

0 comments

Cite this review

Pith. "Pith review of Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving." pith.science (2026). https://pith.science/paper/22BR25DU

@misc{pith2026250311657,
  author       = {Pith},
  title        = {Pith review of: Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/22BR25DU}},
  note         = {Machine review of arXiv:2503.11657}
}

read the original abstract

Large language models have demonstrated remarkable capabilities in natural language processing tasks requiring multi-step logical reasoning capabilities, such as automated theorem proving. However, challenges persist within theorem proving, such as the identification of key mathematical concepts, understanding their interrelationships, and formalizing proofs correctly within natural language. We present KG-prover, a novel framework that leverages knowledge graphs mined from reputable mathematical texts to augment general-purpose LLMs to construct and formalize mathematical proofs. We also study the effects of scaling graph-based, test-time compute using KG-Prover, demonstrating significant performance improvements over baselines across multiple datasets. General-purpose LLMs improve up to 21\% on miniF2F-test when combined with KG-Prover, with consistent improvements ranging from 2-11\% on the ProofNet, miniF2F-test, and MUSTARD datasets. Furthermore, KG-Prover with o4-mini achieves 50\% on pass miniF2F-test. This work provides a promising approach for augmenting natural language proof reasoning with knowledge graphs without the need for additional finetuning.

Figures

Figures reproduced from arXiv: 2503.11657 by the authors.

**Figure 1.** Whereas many modern proof systems focus on training time improvements, we integrate Node retrieval based on an interconnected knowledge graph into our proof system at inference time. Before generating a proof, we inject the most similar nodes into the context, then verify the proof using Lean. If the verification is unsuccessful, we grant the model the chance to traverse the graph deeper, where the knowledge graph … view at source ↗

**Figure 2.** Comparing different depths for the beam search method on a set of parameters that are n = 5, beam width 3, search depth 2. 5.3. Scaling Traversal Depth To allow the model for failure correction and improvement, the graph system has multiple consecutive attempts defined as r. Each attempt allows the model to traverse further in the graph and explore more nodes. 1 2 3 4 5 6 7 20 25 30 35 Accuracy (%) minif2f 1 2 3 4 5… view at source ↗

**Figure 3.** Accuracy increases with greater traversal depth r in the knowledge graph As more proofs get injected into the context and the model gets more tries to correct initial mistakes, the accuracy scales higher per iterative refinement step. This effect is most predominant in smaller parameter models, such as Llama 3.1 8b. This behavior is captured in [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

25 extracted references · 12 canonical work pages

[1]

Anthropic. 2024. https://www.anthropic.com/news/claude-3-5-sonnet Claude 3.5 sonnet model card addendum

work page 2024
[2]

Nearest-neighbor approximation in one-excitation state evolution along spin-1/2 chain governed by XX-Hamiltonian

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

work page Pith review arXiv 2023
[3]

Bansal, S

K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox. 2019. Holist: An environment for machine learning of higher-order theorem proving. In International Conference on Machine Learning (ICML)

work page 2019
[4]

Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin...

arXiv 2020
[5]

de Moura, S

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. 2015. The lean theorem prover (system description). In A. Felty and A. Middeldorp, editors, Automated Deduction – CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378--388. Springer, Cham

work page 2015
[6]

de Moura and S

L. de Moura and S. Ullrich. 2021. The lean 4 theorem prover and programming language. In Proceedings of the In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction

work page 2021
[7]

DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai D...

arXiv 2025
[8]

Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, Arun Rao, Aston Zhang, Aurelien Rodriguez, Austen Gregerson, Ava S...

arXiv 2024

Show all 25 references

[9]

Harrison

J. Harrison. 2009. Hol light: An overview. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 60--66. Springer, Berlin, Heidelberg

2009
[10]

Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. https://arxiv.org/abs/2103.03874 Measuring mathematical problem solving with the math dataset . Preprint, arXiv:2103.03874

2021 arXiv
[11]

Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. 2024. https://arxiv.org/abs/2402.08957 Mustard: Mastering uniform synthesis of theorem and proof data . Preprint, arXiv:2402.08957

2024 arXiv
[12]

Jiang, X

X. Jiang, X. Hong, J. Wang, L. Wang, Q. Li, J. Guo, Z. Jin, and T. Zhao. 2024. Deepseek-prover-v1.5: Integrating reinforcement learning from proof assistant feedback for formal theorem proving. arXiv preprint arXiv:2309.16443

2024 arXiv
[13]

Johnson, D

A. Johnson, D. Baxley, A. Cheung, J. Halbrook, and M. L. Giger. 2020. Mathematics understanding through semantic theory and reasoning development (mustard). In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 13671--13672

2020
[14]

Lample and F

G. Lample and F. Charton. 2022. Deep learning for symbolic mathematics. In Proceedings of the International Conference on Learning Representations (ICLR)

2022
[15]

Neelakantan, T

A. Neelakantan, T. Xu, R. Puri, A. Radford, J. M. Han, et al. 2022. Text and code embeddings by contrastive pre-training. arXiv preprint arXiv:2201.10005

2022 arXiv
[16]

OpenAI. 2024. Gpt-4o mini: Advancing cost-efficient intelligence. OpenAI Blog. Available at: https://openai.com/index/gpt-4o-mini-advancing-cost-efficient-intelligence/

2024
[17]

Peters, Mark Neumann, Mohit Iyyer, Matt Gardner, Christopher Clark, Kenton Lee, and Luke Zettlemoyer

Matthew E. Peters, Mark Neumann, Mohit Iyyer, Matt Gardner, Christopher Clark, Kenton Lee, and Luke Zettlemoyer. 2018. https://doi.org/10.18653/v1/N18-1202 Deep contextualized word representations . In Proceedings of the 2018 Conference of the North A merican Chapter of the As...

2018 doi
[18]

Polu and I

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

2020 arXiv
[19]

ProofWiki . 2025. https://proofwiki.org Proofwiki: An online compendium of mathematical proofs . Accessed: 2025-01-31

2025
[20]

Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowycz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W

Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowycz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W. Kocurek, Ali...

2023 arXiv
[21]

J. Webber. 2012. A programmatic introduction to neo4j. In Proceedings of the 3rd annual conference on Systems, programming, and applications: software for humanity (SPLASH '12)

2012
[22]

Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. https://arxiv.org/abs/2306.15626 Leandojo: Theorem proving with retrieval-augmented language models . Preprint, arXiv:2306.15626

2023 arXiv
[23]

Zheng, J

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

2022 arXiv
[24]

online" 'onlinestring :=

ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...
[25]

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

Pith tools

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

[1] [1]

Anthropic. 2024. https://www.anthropic.com/news/claude-3-5-sonnet Claude 3.5 sonnet model card addendum

work page 2024

[2] [2]

Nearest-neighbor approximation in one-excitation state evolution along spin-1/2 chain governed by XX-Hamiltonian

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

work page Pith review arXiv 2023

[3] [3]

Bansal, S

K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox. 2019. Holist: An environment for machine learning of higher-order theorem proving. In International Conference on Machine Learning (ICML)

work page 2019

[4] [4]

Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin...

arXiv 2020

[5] [5]

de Moura, S

L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. 2015. The lean theorem prover (system description). In A. Felty and A. Middeldorp, editors, Automated Deduction – CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378--388. Springer, Cham

work page 2015

[6] [6]

de Moura and S

L. de Moura and S. Ullrich. 2021. The lean 4 theorem prover and programming language. In Proceedings of the In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction

work page 2021

[7] [7]

DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai D...

arXiv 2025

[8] [8]

Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, Arun Rao, Aston Zhang, Aurelien Rodriguez, Austen Gregerson, Ava S...

arXiv 2024