Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

Anthony Bordg; Haitham Bou Ammar; Jun Wang; Matthieu Zimmer; Rasul Tutunov; Xiaotong Ji

REVIEW 5 major objections 5 minor 1 cited by

Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

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

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

Pith's one-line read By generating and verifying its own intermediate lemmas during search, a 7B-parameter system solves 26 PutnamBench problems, a new best at that scale.

desk verdict A promising wrapper over 7B provers with a genuine subgoal-search idea, but the headline SOTA claim rests on unmatched budgets and a missing ensemble control. read the letter →

arxiv 2507.02726 v1 pith:AUH5WDEC submitted 2025-07-03 cs.AI cs.LG

Matthieu Zimmer , Xiaotong Ji , Rasul Tutunov , Anthony Bordg , Jun Wang , Haitham Bou Ammar This is my paper · ORCID

classification cs.AIcs.LG

keywords self-generatedgoal-conditionedMDPautomatedtheoremprovingLean4MonteCarloTreeSearchPutnamBenchsubgoaldecompositionsampleefficiencylargelanguagemodels

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 sets out to show that the sparse-reward problem in formal theorem proving can be attacked by letting the proof agent generate its own subgoals during search, and that this yields a new state of the art at the 7-billion-parameter scale. It formalizes this as a self-generated goal-conditioned MDP (sG-MDP), where the agent may create a Lean conjecture at any point and is rewarded when such conjectures are independently verified. Its instantiation, Bourbaki (7B), combines two 7B LLMs with an MCTS-style search over a stack of goals, and reports solving 26 of 658 PutnamBench problems at pass@512, beating previous 7B/8B results that used larger sample budgets. If the result holds, smaller models become a practical route to competition-level formal proofs.

What carries the argument

The central object is the self-generated goal-conditioned MDP (sG-MDP), a goal-conditioned MDP augmented with a goal stack: an action can either be a primitive Lean tactic or a newly proposed conjecture, where primitive actions only transition the proof state when they solve the top goal, and proposing a conjecture pushes that conjecture onto the stack. The search machinery is an MCTS variant whose node value is initialized by a reward combining progress on the original goal with progress on generated subgoals, and whose selection uses UCB over the empirical mean; PyPantograph validates tactics and verifies goals and subgoals inside Lean 4. The key work is that the reward becomes denser while remaining grounded in verifier feedback, so the search does not need a learned critic.

What would settle it

Repeat Bourbaki's PutnamBench evaluation on the fixed 658-problem version with several random seeds, and also run the same two base models under the same MCTS but with the conjecture-reward term disabled; if a fresh Bourbaki run scores 23 or below, or if removing the subgoal reward leaves the solved count unchanged, the central claim fails.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that a theorem-prover can profitably treat intermediate lemmas as actions: instead of a preset goal distribution, the transition function lets the agent push a newly proposed conjecture onto a goal stack and then use every primitive tactic as an attempt to solve the top goal. MCTS then explores this state-goal graph, and the value of a node is computed entirely from verified outcomes—how many locally introduced conjectures were confirmed and how far the proof advanced—rather than from a learned critic. The authors report that this enabled their ensemble Bourbaki (7B) to solve 26/658 PutnamBench problems at pass@512, compared with 23/658 for DeepSeek-Prover-V2 at a larger sample budget and 10/644 for Kimina-7B, and that applying the wrapper to STP and DeepSeek-Prover-V2 produced additional solved theorems at matched budgets. They interpret this as evidence that self-generated subgoals make proof search more sample-efficient and more diverse.

Load-bearing premise

The comparison that makes the claim a new state of the art assumes that one run scoring 26/658 genuinely beats 23/658 on the same fixed problem set, rather than reflecting the benchmark's version change, the two-model ensemble, or run-to-run variance.

Editorial extensions

If this is right

At the 7B-8B scale, search with self-generated subgoals completes more PutnamBench proofs than prior whole-proof and tree-search baselines, including models that used larger sample budgets.
Wrapping an existing prover in the sG-MDP framework yields extra completed proofs at the same sample budget: STP goes from 6 to 7 at pass@64 and 7 to 8 at pass@128, while DeepSeek-Prover-V2 goes from 15 to 23 at pass@128.
Subgoal generation supplies a denser, verifier-based reward signal that can replace or complement learned critics in MCTS-based theorem proving.
The framework is modular: as long as a policy can emit valid Lean conjectures and tactics, other base models can be ensembled or swapped in.
Because the rewards are computed from Lean verification alone, the proof fragments counted by the search are machine-checked rather than merely plausible.

Reading between the lines

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

In my reading, the reported gain over the previous best is a 3-problem margin from a single run with no reported variance, so the state-of-the-art claim should be treated as provisional until reproduced across seeds on a fixed benchmark version.
The mechanism predicts a testable scaling pattern: the advantage over whole-proof sampling should be largest on problems that admit a useful intermediate 'have' step, and should shrink on problems with a flat proof structure.
The same formulation could be lifted to other tactic-based proof assistants, such as Isabelle or Coq, wherever a verifier interface analogous to PyPantograph can expose goal states and conjecture validation.
Because the value signal comes from verifier feedback, training an RL policy directly on the sG-MDP rewards, as the paper notes is possible, could convert the search-time gains into one-shot model capabilities without new proof corpora.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

The thing to know: Bourbaki is a real, buildable idea — generate subgoals as Lean 'have' statements, verify them during MCTS, and use that as dense reward. That is worth reading. But the headline comparison is shakier than it looks: the 26/658 vs 23/658 margin is a single run, the sample-budget column mixes units, and there is no control that isolates the search wrapper from the two-model ensemble.

What's genuinely new is the sG-MDP framing and the reward from verified conjectures rather than a learned critic. The implementation is described cleanly: Pantograph, Lean 4, vLLM, N=10, K=512, and an honest footnote about the 644 vs 658 benchmark versions. Table 2 is the most useful evidence: applying the wrapper to STP and to DeepSeek-Prover-v2 as single base models gives 7 vs 6, 8 vs 7, and 23 vs 15 at 128. That suggests the subgoal mechanism itself does something, not just ensembling.

The soft spots are real. The load-bearing one is that 'sample budget' isn't a matched budget. An MCTS iteration can call the model many times: up to N tactic candidates plus a completion step for heuristic tactics like apply?. Comparing K=512 iterations to pass@1024 whole-proof generations overstates sample efficiency, and Table 2's '128 vs 128' has the same unit problem. So the paper's claim that the method 'completes more proofs with fewer samples' is not established. Second, there is no ensemble-only control; part of the 26 could be the union of each base model's best whole-proof generations. Table 2 mitigates this for single models, but not with matched units. Third, single run, no error bars; 26 vs 23 is three problems, within plausible noise. Fourth, no code release.

None of this kills the idea. The sG-MDP formulation is a reasonable way to think about subgoal-conditioned search, and the verified-conjecture reward is a nice alternative to learned critics. But the empirical claims need version-matched, budget-matched controls, repeated runs, and code before I'd call it SOTA.

Who is this for? Researchers working on LLM-based theorem proving and anyone interested in search wrappers over small open models. It deserves a serious referee — the idea is worth building on and the authors are transparent about known limitations — but the review should demand the missing controls.

Recommendation: send to peer review, but expect revision.

Referee Report

5 major / 5 minor

Summary. The paper introduces self-generated goal-conditioned MDPs (sG-MDPs), a formalism for theorem proving in which an LLM proposes subgoals during proof search, and applies MCTS-like search with rewards derived from Lean verification and solved conjectures. The system, Bourbaki (7B), ensembles DeepSeek-Prover-v2-7B and Kimina-7B and is evaluated on PutnamBench. The authors report 26/658 solved problems at an MCTS budget of 512, claiming a new 7B state of the art and improved sample efficiency over whole-proof baselines, plus additional improvements when wrapping STP and DeepSeek-Prover-v2.

Significance. If the empirical claims were properly controlled, the sG-MDP formalism and the verifier-based subgoal reward could be a useful framework for dense reward in neural theorem proving. The use of Lean verification instead of a learned critic is an attractive simplification, and the modular ensembling design is a strength. However, the current evidence does not support the causal claim that goal-conditioned search, rather than ensembling or additional model calls, produces the improvement. The single-run, small-margin headline result and the mixed benchmark denominators further limit confidence. The contribution is therefore potentially significant but not yet substantiated.

major comments (5)

[Section 4, Table 1] The headline comparison lacks an ensemble/no-search control. Bourbaki (7B) is built by ensembling DeepSeek-Prover-v2-7B and Kimina-7B (Section 1), but Table 1 compares Bourbaki against these models individually. Without a control that runs the same two-model ensemble under whole-proof generation, the 26/658 result cannot be attributed to sG-MDP goal-conditioned search; it may simply be the union of the base models' best whole-proof generations plus extra sampling. The observation that 'some new theorems at pass@512 are not found at pass@1024 using the base models' does not replace this control, because the base models were not run as an ensemble and not at a matched budget.
[Section 4, Tables 1 and 2] The 'sample budget' is not a matched comparison. Each of K=512 MCTS iterations consumes multiple LLM calls: tactic sampling with N=10 candidates, subgoal proposal, and, for heuristic tactics such as apply?, a full base-model completion (as stated in the Implementation Details). Comparing this to pass@1024 whole-proof generations in Table 1, or to pass@64/128 in Table 2, therefore does not establish sample efficiency. The paper should report a common unit such as total LLM calls or model-compute-equivalent samples.
[Section 4, Table 1] The headline margin is a single run with no error bars. Bourbaki solves 26/658 versus DeepSeek-Prover-v2's 23/658; with no repeated seeds or variance estimates, a 3-problem difference cannot be distinguished from run-to-run noise. The table also mixes benchmark versions: the footnote states that some prior results used the 644-problem version, but the table's denominators are 644 and 658 (e.g., Kimina 10/644 vs Bourbaki 26/658). The comparison should be made on a single frozen version with confidence estimates.
[Section 4, Implementation Details] The handling of heuristic tactics through a fallback base-model completion is a potential confound. The paper states that tactics such as apply? are finished by 'the plain base model to complete the remainder of the proof.' If many of the 26 solved proofs are completed by this fallback, the improvement may come from the base model rather than from sG-MDP search. The authors should report how many solved proofs required the fallback and verify that the claimed gains survive when the fallback is omitted or separately ablated.
[Section 3.2 and Eq. (1)] The objective used in the experiments is underspecified. Equation (1) defines the reward as R(st, ¯g0) + λ R(st, ¯gt), but Section 3.2 states that the initial value of a node is R(st, ¯gt) and backpropagation uses R(st, ¯gt), and the Implementation Details say the value is 'a combination of depth-based metrics and the number of solved conjectures' without giving the formula. The paper should specify the exact reward and value-update equations used to produce Tables 1 and 2.

minor comments (5)

[Section 1 and Table 1] The statement that Kimina-7B is the previous 7B state of the art with 10/644 should be reconciled with the 658-problem version of the benchmark; the caption should state the version for every row.
[Section 3.1] The definitions of IsGoal, ToGoal, and Solves overlap with the reward function; it is also unclear what happens to the transition when RemoveLast is applied to an empty goal stack.
[Section 4] The term pass@k is used for the MCTS system, but k is not defined in that context; the authors should state explicitly whether k counts MCTS iterations, expanded nodes, or LLM calls.
[Section 4] The notation is inconsistent: the text refers to both 'DeepSeek-V2-7B' and 'DeepSeek-Prover-v2-7B' for the same model.
[Related Work] The related-work paragraph on MCTS contains citation and punctuation errors, for example 'AlphaProof (2024); Xin et al. (2024). (Han et al., 2022)', which should be corrected.

Circularity Check

0 steps flagged · score 0.0 of 10

No internal circularity: verified-proof outcomes are not pre-fitted inputs.

full rationale

No load-bearing reduction was found. The paper's central objects, sG-MDP, subgoal rewards, and MCTS tree search, are all defined from Lean state transitions and verifier feedback (Sections 3.1 and 3.2), and the reported pass counts are outcomes of type-checked proofs rather than fitted constants or renamed inputs. The base models (DeepSeek-Prover-v2 and Kimina-7B) are external checkpoints, not tuned to PutnamBench by this work, and no parameter is fit to the 26/658 result. The sG-MDP transition and reward definitions (Eq. 1) do not presuppose the solved-theorem count; Solves is computed by Lean verification. No uniqueness theorem from the authors' prior work is invoked, and the citations to Pantograph, LeanDojo, and the base models are external support rather than a self-citation chain. The manuscript's own caveats, the footnote that earlier results used the 644-problem version, the single-run evaluation without error bars, and the stated plan to improve soundness of heuristic-tactic handling, are experimental rigor limitations, not circularity. The missing ensemble/no-search control and the sample-budget unit mismatch (K=512 MCTS iterations versus pass@1024 whole proofs) are threats to the empirical comparison and should be counted under correctness risk; under the hard rule requiring an exhibited reduction between the claimed prediction and an input, they do not constitute circularity. Overall, the derivation is self-contained against external benchmarks.

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

The central claim depends on five hyperparameters (C, lambda, reward weights, N, K), three of which are unspecified; the software stack is a domain assumption; the base model quality is an empirical assumption. No invented physical entities are introduced, so that list is empty.

free parameters (5)

C (UCB exploration constant)
Controls exploration-exploitation in Section 3.2; no value is given in the paper, so reproducibility requires guessing.
lambda (subgoal reward weight)
Appears in Eq. (1) as the trade-off between the initial goal reward and the subgoal reward; the paper does not state whether it is used in the MCTS reward and, if so, its value.
reward combination weights for depth and solved conjectures
Section 4 says the value uses 'a combination of depth-based metrics and the number of solved conjectures' but gives no formula or weights.
N (tactic candidates per node) = 10
Given in Section 4; a search-budget hyperparameter.
K (MCTS iterations) = 512
Given in Section 4; a search-budget hyperparameter.

assumptions (4)

domain assumption The sG-MDP transition and reward functions are a faithful formalization of Lean proof search with 'have' statements.
Section 3.1 maps tokens, tactics, and conjectures to the MDP tuple; the validity of this mapping is assumed, not proven.
domain assumption PyPantograph v0.3.2 with Lean 4.20.1 and mathlib v4.20.1 correctly validates tactics and 'have' conjectures.
Section 4 states the software stack; the correctness of the verifier backend is taken for granted.
standard math MCTS with UCB is a sound search procedure for this MDP.
Uses standard UCB selection without proof of convergence in this setting.
domain assumption The base models (DeepSeek-Prover-v2-7B, Kimina-7B, STP) generate useful tactic and subgoal proposals with sufficient diversity.
The whole pipeline depends on the policy model's proposal quality; this is argued empirically, not guaranteed.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving." pith.science (2026). https://pith.science/paper/AUH5WDEC

@misc{pith2026250702726,
  author       = {Pith},
  title        = {Pith review of: Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AUH5WDEC}},
  note         = {Machine review of arXiv:2507.02726}
}

read the original abstract

Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.

Figures

Figures reproduced from arXiv: 2507.02726 by the authors.

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

The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
cs.AI 2026-04 unverdicted novelty 6.0 of 10

The topological dual of a dataset is introduced as a transformation that encodes logical structures into topological ones to expose invariants in neural latent spaces for AlphaGeometry-style reasoning.

Reference graph

Works this paper leans on

20 extracted references · 7 canonical work pages · cited by 1 Pith paper

[1]

Ai achieves silver-medal standard solving international mathematical olympiad problems

AlphaGeometry Team AlphaProof. Ai achieves silver-medal standard solving international mathematical olympiad problems. 2024. URL https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

work page 2024
[2]

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

Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\ 104--123. Springer, 2025

work page 2025
[3]

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

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

work page 2025
[4]

Abel: Sample efficient online reinforcement learning for neural theorem proving

Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024

work page 2024
[5]

Ayers, and Stanislas Polu

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models, 2022. URL https://arxiv.org/abs/2102.06203

arXiv 2022
[6]

Hypertree proof search for neural theorem proving, 2022

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving, 2022. URL https://arxiv.org/abs/2205.11491

arXiv 2022
[7]

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

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

arXiv 2025
[8]

Goal-conditioned reinforcement learning: Problems and solutions, 2022

Minghuan Liu, Menghui Zhu, and Weinan Zhang. Goal-conditioned reinforcement learning: Problems and solutions, 2022. URL https://arxiv.org/abs/2201.08299

arXiv 2022

Show all 20 references

[9]

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

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

2025 arXiv
[10]

Universal value function approximators

Tom Schaul, Daniel Horgan, Karol Gregor, and David Silver. Universal value function approximators. In Francis Bach and David Blei (eds.), Proceedings of the 32nd International Conference on Machine Learning, volume 37 of Proceedings of Machine Learning Research, pp.\ 1312--132...

2015
[11]

Putnambench: A multilingual competition-mathematics benchmark for formal theorem-proving

George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: A multilingual competition-mathematics benchmark for formal theorem-proving. In AI for Math Workshop@ ICML 2024, 2024

2024
[12]

DT -solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function

Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. DT -solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Anna Rogers, Jord...

2023
[13]

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

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

2025 arXiv
[14]

Internlm2

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

Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcem...

2024 arXiv
[16]

Leandojo: Theorem proving with retrieval-augmented language models

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

2023
[17]

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...
[18]

@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 ...
[19]

\@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...
[20]

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

Pith tools

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

[1] [1]

Ai achieves silver-medal standard solving international mathematical olympiad problems

AlphaGeometry Team AlphaProof. Ai achieves silver-medal standard solving international mathematical olympiad problems. 2024. URL https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

work page 2024

[2] [2]

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

Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\ 104--123. Springer, 2025

work page 2025

[3] [3]

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

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

work page 2025

[4] [4]

Abel: Sample efficient online reinforcement learning for neural theorem proving

Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. Abel: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024

work page 2024

[5] [5]

Ayers, and Stanislas Polu

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models, 2022. URL https://arxiv.org/abs/2102.06203

arXiv 2022

[6] [6]

Hypertree proof search for neural theorem proving, 2022

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving, 2022. URL https://arxiv.org/abs/2205.11491

arXiv 2022

[7] [7]

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

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

arXiv 2025

[8] [8]

Goal-conditioned reinforcement learning: Problems and solutions, 2022

Minghuan Liu, Menghui Zhu, and Weinan Zhang. Goal-conditioned reinforcement learning: Problems and solutions, 2022. URL https://arxiv.org/abs/2201.08299

arXiv 2022