Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

StepFun-Prover Preview: Let's Think and Verify Step by Step

T0 review · 3 major / 4 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 The paper reports a training pipeline that lets a language model decide when and how to query the Lean 4 verifier, and claims that the resulting 32B model reaches 70.0% pass@1 on miniF2F-test—above the previously published results from…

desk verdict A new SOTA number on miniF2F with a believable training story, but the comparison is only as good as the benchmark variant, and that variant is underspecified. read the letter →

arxiv 2507.20199 v3 pith:IBCFVWUK submitted 2025-07-27 cs.AI

Shijie Shang , Ruosi Wan , Yue Peng , Yutong Wu , Xiong-hui Chen , Jie Yan , Xiangyu Zhang This is my paper · ORCID
classification cs.AI
keywords formaltheoremprovingLean4reinforcementlearningtool-integratedreasoningminiF2FGRPOpass@1verifierfeedback
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 reports a way to train a large language model that solves formal proofs by interacting with the Lean 4 proof assistant while it thinks. The model is free to emit partial Lean code, read back the verifier's error messages, revise, and try again before giving a final proof, with no fixed script for how many interactions to use. Trained with supervised warm-up followed by reinforcement learning whose only reward is whether the final proof verifies, the resulting 32B-parameter model reaches a pass@1 of 70.0% on the corrected miniF2F-test benchmark using 32 sampled attempts per problem. That figure is higher than the previously published results for a 72B-parameter prover (63.9%) and a 671B-parameter prover (61.9%) on the same benchmark. The paper's broader claim is that letting the model drive its own tool use, guided by verifier feedback, is a practical route to efficient automated theorem proving.

What carries the argument

The carrier of the argument is the tool-integrated rollout: a hybrid trajectory of the form natural-language reasoning, a Lean 4 sketch enclosed in <sketch> and </sketch>, the verifier's output enclosed in <REPL> and </REPL>, repeated until a final proof is emitted after a </think> delimiter. Each time the model closes a sketch, generation pauses, the snippet is sent to a wrapped Lean 4 REPL, and messages (errors, goals, sorries, or success) are returned as tokens the model can read. Training uses GRPO with a binary reward of 1 only when the final proof verifies and 0 otherwise, with the verifier-feedback tokens masked out of the loss so the model is trained only on its own reasoning. Around this mechanism sits a pipeline: a cold-start dataset built from formal corpora and autoformalized word problems, filtered for tautological, contradictory, or ill-posed statements; a fusion step that corrects wrong proofs from an existing 72B prover to harmonize response styles; an iterative RL-SFT cycle that re-trains on successful trajectories from problems of intermediate difficulty; and an asynchronous remote server that runs over a thousand REPL processes in parallel, making multi-turn reinforcement learning feasible.

What would settle it

Build a held-out set of formal statements of comparable difficulty that are provably absent from the training corpora, run the released 32B model with the same 32-sample protocol, and compare pass@1. If the score falls to the level of the previous baselines, the headline number is largely memorization rather than learned tool-integrated reasoning. A cheaper check is to diff the miniF2F-test statements against the three training corpora for exact or near-duplicate statements.

Watch

Extended reading notes

Core claim

The central claim is that a proof-generating model can learn, end to end, to interleave natural-language reasoning with Lean 4 code sketches and live verifier feedback, and that this tool-integrated behavior transfers to a benchmark. The trained 32B model solves 70.0% of the problems on the corrected miniF2F-test at pass@1 with 32 generations per problem, while its 7B sibling reaches 66.0%. The paper argues these results come from the training pipeline rather than from larger scale: the same approach is presented as the reason the 32B model outperforms substantially larger prior provers, and longer generation limits (more room for reflection and interaction) push performance from 58.3% at 4096 tokens to 70.0% at 20480 tokens. The authors also observe emergent interaction habits, such as resolving warnings proactively, restructuring a proof when a tactic times out, and refining a solution after reading feedback.

Load-bearing premise

The load-bearing premise is that the corrected miniF2F-test set is a fair, uncontaminated measure of proving ability, and specifically that its problems were not present in the training data; the paper does not document train/test disjointness or the corrections applied.

Editorial extensions

If this is right

  • Longer allowed generation length improves pass@1 monotonically on miniF2F-test, from 58.3% at 4096 tokens to 70.0% at 20480 tokens, so spending more generated tokens on check-and-revise behavior buys accuracy.
  • A 32B-parameter model trained this way can exceed the reported pass@1 of a 671B-parameter prover, so agentic use of verifier feedback can substitute for parameter count at this task.
  • The reward signal does not need to grade partial progress: binary outcome-based reward on final verification, combined with feedback tokens, is sufficient for the model to learn multi-step repair behavior.
  • The pipeline is presented as a general end-to-end framework for tool-integrated reasoning, applicable beyond formal mathematics to any setting where an environment returns reliable signals.

Reading between the lines

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

  • Because the paper does not state that the corrected miniF2F-test problems are disjoint from the three training sources it lists (the workbook corpus, the self-play theorem-proving dataset, and autoformalized word problems), a portion of the 70.0% could reflect memorization; an independent contamination audit would settle this.
  • Pass@1 at 32 samples does not count the compute spent on REPL round-trips and re-generation inside each trajectory, so the efficiency gain relative to sampling-heavy baselines should be measured in total Lean calls or total tokens per solved problem, not just passes per sample.
  • The same training recipe could be tested on harder held-out problem sets, for example competition problems not present in any training corpus, to see whether the tool-integrated behavior generalizes rather than overfitting to benchmark idioms.
  • A natural extension, not explored here, is to give the model credit for intermediate milestones, such as clearing an error or closing a goal, through dense reward shaping, which could speed up learning beyond the binary final-proof reward.
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.

Referee Report

3 major / 4 minor

Summary. This technical report presents StepFun-Prover, a family of Lean 4 theorem-proving LLMs (7B and 32B) trained through cold-start supervised fine-tuning, response-pattern fusion, and tool-integrated GRPO with real-time Lean4-REPL feedback. The main empirical claim is a pass@1 of 70.0% on the miniF2F-test benchmark with 32 responses per problem, which the authors state surpasses DeepSeek-Prover-V2-671B (61.9%) and Kimina-Prover-72B (63.9%). The paper also contributes a training pipeline, an iterative RL-SFT cycle, and a detailed example of tool-integrated reasoning.

Significance. If the empirical claim survives scrutiny, the result would be practically significant: a 32B model outperforming the much larger DeepSeek-Prover-V2-671B with relatively few samples suggests that tool-integrated RL is a promising direction for automated theorem proving. The paper is also commendable for announcing release of model weights and for including a concrete example of REPL-driven proof repair. However, the significance is currently bounded by three issues: (i) the use of an uncircumscribed corrected miniF2F variant while baselines are borrowed from original papers, (ii) the absence of a train/test disjointness statement, and (iii) the lack of uncertainty quantification. These issues are fixable but must be addressed before the SOTA claim can be accepted.

major comments (3)
  1. [§3.1, Table 1] The central SOTA comparison is not apples-to-apples. The text states that evaluation is done on 'Numina's corrected miniF2F benchmark from their HuggingFace repository,' while all baseline numbers are 'sourced from their respective original papers.' The corrections are never specified, and no baseline is re-run on the same corrected instance. If the corrected benchmark changes problem statements, the Lean/Mathlib version (the paper states Lean 4.20.0 for its own runs but not for the baselines), or the problem list, the reported margin of 6.1–8.1 percentage points could be an artifact of the benchmark instance rather than of model capability. The authors should either supply a diff of the corrections, re-run the baselines on the identical corrected benchmark with an identical protocol, or downgrade the superiority claim accordingly.
  2. [§2.1 and §3.1] The paper does not state that the training corpora (Lean Workbook, STP, and autoformalized Numina problems) are disjoint from the corrected miniF2F test set. Because miniF2F is a public benchmark with substantial overlap with datasets commonly used for formalization, and the paper does not report deduplication, the 70.0% figure remains open to a memorization-based explanation. Please report the exact deduplication procedure (or a hash-based overlap analysis) against the test problems, and/or validate on an entirely disjoint benchmark such as ProofNet.
  3. [§3.1, Table 1] No uncertainty quantification is reported. Pass@1 is estimated from 32 responses per problem; with a test set of roughly 244 problems, the standard error of the difference between 70.0% and 63.9% is on the order of 4 percentage points, so the claimed 'over 4%' superiority margin is within roughly 1.5 standard errors. The paper should report per-problem pass rates, confidence intervals (e.g., bootstrap), or a paired comparison of the models on the same problem set.
minor comments (4)
  1. [Related Work] The phrase 'OpenAI o-seriers' should be 'OpenAI o-series'.
  2. [Figure 1 caption] The spelling 'Stepfun-Prover' conflicts with 'StepFun-Prover' in the text, and the caption should define pass@1, the number of responses per problem, and the sampling budget used for the baseline methods.
  3. [§2.4, Eq. (1)] The group-based advantage divides by the standard deviation of the reward group, which can be zero when all sampled rewards are equal; please specify the behavior in that case (e.g., set the advantage to 0).
  4. [§3.1] For reproducibility, please provide the exact commit or date of Numina's corrected miniF2F repository, the evaluation harness, and the generated proofs for all problems.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the 70.0% pass@1 is an externally verified benchmark result, not a constructional consequence of the paper's own inputs.

full rationale

The paper makes no derivation-from-inputs claim that would be circular. The central result, 70.0% pass@1 on miniF2F-test, is obtained by running the trained model against an external Lean 4 benchmark and checking proofs with the Lean REPL; the training pipeline (cold-start SFT, response-pattern fusion, GRPO with binary REPL reward, iterative RL-SFT) optimizes on training corpora (Lean Workbook, STP, autoformalized Numina Math 1.5) and does not fit any parameter to miniF2F-test. The only self-citation, to Open-Reasoner-Zero [14] which shares co-author Xiangyu Zhang, supports the implementation choice of omitting KL regularization in GRPO; that choice is not load-bearing for the benchmark claim. Two validity concerns remain, but they are not circularity by construction: (i) the own-model evaluation uses 'Numina's corrected miniF2F benchmark from their HuggingFace repository' while baseline numbers are 'sourced from their respective original papers', so the comparative SOTA claim may not be apples-to-apples; and (ii) the paper never states that miniF2F-test statements are disjoint from the training corpora, leaving a memorization or contamination risk. These affect external validity and benchmark comparability, not whether the reported result reduces to its own inputs. I therefore find no circular step.

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

The central claim is an empirical benchmark result, so the ledger primarily records assumptions about the evaluation setup and data hygiene. There are no new mathematically invented entities. The free parameters are training and evaluation hyperparameters that directly affect the reported number, most importantly the 32-sample pass@1 estimator and the maximum generation length.

free parameters (4)
  • Number of generated responses per problem (pass@1 estimator) = 32
    The reported pass@1 is estimated from 32 samples per problem. The choice affects the point estimate, and no variance is reported.
  • Maximum generation length = 20480 tokens
    Performance varies with maximum generation length (from 58.3% at 4096 to 70.0% at 20480), so the final result depends on this hand-chosen budget.
  • Success-rate filter interval for RL training prompts = (0, 1)
    Prompts are retained only if their per-prompt success rate lies strictly between 0 and 1, a hand-chosen threshold that shapes the training distribution.
  • Sampling temperature and top-p = 1.0 and 0.999
    These sampling hyperparameters are used in both RL rollout and evaluation, chosen to encourage exploration.
assumptions (4)
  • standard math Lean 4 verifier correctly determines proof validity
    The binary reward and final evaluation assume that REPL verification is a reliable oracle for mathematical correctness.
  • domain assumption Numina's corrected miniF2F is a valid test set for general theorem proving
    The paper evaluates on 'Numina's corrected miniF2F' without specifying what corrections were made or how they affect difficulty compared to the standard benchmark.
  • domain assumption Training data does not overlap with miniF2F-test
    The paper does not state that the benchmark problems were excluded from the training corpora (Lean Workbook, STP, autoformalized Numina). This is a key premise for interpreting the result as general proving ability rather than memorization.
  • domain assumption Baseline results from original papers are comparable
    Baselines were evaluated under possibly different settings (notably at least 32K token context) yet are directly compared to StepFun-Prover's numbers, assuming the differences do not affect the comparison.

how reviews work

0 comments
Cite this review

Pith. "Pith review of StepFun-Prover Preview: Let's Think and Verify Step by Step." pith.science (2026). https://pith.science/paper/IBCFVWUK

@misc{pith2026250720199,
  author       = {Pith},
  title        = {Pith review of: StepFun-Prover Preview: Let's Think and Verify Step by Step},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IBCFVWUK}},
  note         = {Machine review of arXiv:2507.20199}
}
abstract

We present StepFun-Prover Preview, a large language model designed for formal theorem proving through tool-integrated reasoning. Using a reinforcement learning pipeline that incorporates tool-based interactions, StepFun-Prover can achieve strong performance in generating Lean 4 proofs with minimal sampling. Our approach enables the model to emulate human-like problem-solving strategies by iteratively refining proofs based on real-time environment feedback. On the miniF2F-test benchmark, StepFun-Prover achieves a pass@1 success rate of $70.0\%$. Beyond advancing benchmark performance, we introduce an end-to-end training framework for developing tool-integrated reasoning models, offering a promising direction for automated theorem proving and Math AI assistant.

Figures

Figures reproduced from arXiv: 2507.20199 by the authors.

Figure 1
Figure 1. Performance comparison on MiniF2F-test. y-axis shows the pass@1, which is computed [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Our training pipeline. Left. Tool-integrated RL and iterative RL-SFT cycle. The upper [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Training reward and test accuracy (pass@1) of the tool-integrated GRPO. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: REPL interaction frequency distribution 3.2.2. Diverse Reasoning Patterns Through our tool-integrated reinforcement learning framework with cold start, StepFun-Prover￾Preview develops several advanced reasoning capabilities that leverage real-time environment feedback,…

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. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

Reference graph

Works this paper leans on

39 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    Openai o1 system card

    Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. Openai o1 system card. arXiv preprint arXiv:2412.16720, 2024

    arXiv 2024

  2. [2]

    DeepSeek-R1: Incentivizing reasoning capability in llms via reinforcement learning

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. DeepSeek-R1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025

    arXiv 2025

  3. [3]

    QwQ: Reflect deeply on the boundaries of the unknown

    Qwen Team. QwQ: Reflect deeply on the boundaries of the unknown. https://qwenlm .github.io/blog/qwq-32b-preview, 2024

    work page 2024

  4. [4]

    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, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Paga...

    arXiv 2025

  5. [5]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXi...

    arXiv 2025

  6. [6]

    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, and Chi Jin. Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025

    arXiv 2025

  7. [7]

    Solving formal math problems by decomposition and iterative reflection

    Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, and Hang Li. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507.15225, 2025

    arXiv 2025

  8. [8]

    Kimina-Prover: Applying test-time rl search on large formal reasoning models, 2025

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Thibaut Barroyer, Ebony Zhang, Bolton Bailey, Frederick Pu, Marina Vinyes, Zhengying Liu, and Jia Li. Kimina-Prover: Applying test-time rl search on large formal reasoning models, 2025

    work page 2025

Show all 39 references
  1. [9]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer, 2021

    2021

  2. [10]

    Lean Work- book: A large-scale Lean problem set formalized from natural language math problems

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Zheng Yuan, Dahua Lin, and Kai Chen. Lean Work- book: A large-scale Lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024

    2024 arXiv

  3. [11]

    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 preprint arXiv:2502.00212, 2025. 10 Technical Report

    2025 arXiv

  4. [12]

    Deepseek-V3 technical report

    Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. Deepseek-V3 technical report. arXiv preprint arXiv:2412.19437, 2024

    2024 arXiv

  5. [13]

    System card: Claude Opus 4 & Claude Sonnet 4

    Anthropic. System card: Claude Opus 4 & Claude Sonnet 4. https://www-cdn.anthr opic.com/4263b940cabb546aa0e3283f35b686f4f3b2ff47.pdf, 2025

    2025

  6. [14]

    Open-Reasoner-Zero: An open source approach to scaling up reinforcement learning on the base model

    Jingcheng Hu, Yinmin Zhang, Qi Han, Daxin Jiang, Xiangyu Zhang, and Heung-Yeung Shum. Open-Reasoner-Zero: An open source approach to scaling up reinforcement learning on the base model. arXiv preprint arXiv:2503.24290, 2025

    2025 arXiv

  7. [15]

    A read-eval-print-loop for lean 4

    Lean FRO. A read-eval-print-loop for lean 4. https://github.com/leanprover- community/repl

  8. [16]

    Salvatore Sanfilippo. Redis. https://redis.io

  9. [17]

    Introducing openai o3 and o4-mini

    OpenAI. Introducing openai o3 and o4-mini. https://openai.com/index/introduci ng-o3-and-o4-mini/ , 2025

    2025

  10. [18]

    QwQ-32b: Embracing the power of reinforcement learning

    Qwen Team. QwQ-32b: Embracing the power of reinforcement learning. https://qwen lm.github.io/blog/qwq-32b/, 2025

    2025

  11. [19]

    Hypertree proof search for neural theorem proving

    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. In Advances in Neural Information Processing Systems, NeurIPS 2022, 2022

    2022

  12. [20]

    Formal mathematics statement curriculum learning

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022

    2022 arXiv

  13. [21]

    AI achieves silver-medal standard solving international mathematical olympiad problems

    Google DeepMind. AI achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ai-solves-imo -problems-at-silver-medal-level/ , 2024

    2024

  14. [22]

    InternLM2.5-StepProver: Advancing automated theorem proving via expert iteration on large-scale lean problems

    Zijian Wu, Suozhi Huan, 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. [23]

    Scalable best-first tree search for llm-based automatic theorem proving

    Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025

    2025

  16. [24]

    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

    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 feed- back for reinforcem...

    2024 arXiv

  17. [25]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910, 2023

    2023 arXiv

  18. [26]

    Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample

    Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022. 11 Technical Report

    arXiv

  19. [27]

    LEGO-Prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. LEGO-Prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023

    arXiv

  20. [28]

    Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities

    Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabil...

    2025 arXiv

  21. [29]

    Competitive programming with large reasoning models

    Ahmed El-Kishky, Alexander Wei, Andre Saraiva, Borys Minaiev, Daniel Selsam, David Dohan, Francis Song, Hunter Lightman, Ignasi Clavera, Jakub Pachocki, et al. Competitive programming with large reasoning models. arXiv preprint arXiv:2502.06807, 2025

    2025 arXiv

  22. [30]

    Introducing Codex

    OpenAI. Introducing Codex. https://openai.com/index/introducing-codex/ , 2025

    2025

  23. [31]

    Simpletir: End-to-end reinforcement learning for multi-turn tool-integrated reasoning

    Zhenghai Xue, Longtao Zheng, Qian Liu, Yingru Li, Zejun Ma, and Bo An. Simpletir: End-to-end reinforcement learning for multi-turn tool-integrated reasoning. https://si mpletir.notion.site/report, 2025. Notion Blog

    2025

  24. [32]

    Agentic reasoning and tool integration for llms via reinforcement learning

    Joykirat Singh, Raghav Magazine, Yash Pandya, and Akshay Nambi. Agentic reasoning and tool integration for llms via reinforcement learning. arXiv preprint arXiv:2505.01441, 2025

    2025 arXiv

  25. [33]

    Nemotron-Research-Tool-N1: Tool-using language models with reinforced reasoning

    Shaokun Zhang, Yi Dong, Jieyu Zhang, Jan Kautz, Bryan Catanzaro, Andrew Tao, Qingyun Wu, Zhiding Yu, and Guilin Liu. Nemotron-Research-Tool-N1: Tool-using language models with reinforced reasoning. arXiv preprint arXiv:2505.00024, 2025

    2025 arXiv

  26. [34]

    ReTool: Reinforcement learning for strategic tool use in llms

    Jiazhan Feng, Shijue Huang, Xingwei Qu, Ge Zhang, Yujia Qin, Baoquan Zhong, Chengquan Jiang, Jinxin Chi, and Wanjun Zhong. ReTool: Reinforcement learning for strategic tool use in llms. arXiv preprint arXiv:2504.11536, 2025

    2025 arXiv

  27. [35]

    ToRL: Scaling tool-integrated rl

    Xuefeng Li, Haoyang Zou, and Pengfei Liu. ToRL: Scaling tool-integrated rl. arXiv preprint arXiv:2503.23383, 2025

    2025 arXiv

  28. [36]

    Goedel-Prover-V2: The strongest open-source theorem prover to date, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover-V2: The strongest open-source ...

    2025

  29. [37]

    messages

    Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, and Kun Gai. Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. arXiv preprint arXiv:2507.08649, 2025. 12 Technic...

    2025 arXiv

  30. [38]

    * (z + x) * (x + y) + (y ^ 2 - x ^ 2) * (y + z) * (x + y) + (z ^ 2 - y ^ 2) * (y + z) * (z + x)) /\n ((y + z) * (z + x) * (x + y))\nnum_eq :\n (x ^ 2 - z ^ 2) * (z + x) * (x + y) + (y ^ 2 - x ^ 2) * (y + z) * (x + y ) + (z ^ 2 - y ^ 2) * (y + z) * (z + x) =\n (x ^ 2 - z ^ 2) *...

  31. [39]

    , 250 "endPos

    + z ^ 4 + y ^ 4", 250 "endPos": {"line": 31, "column": 9} 251 } 252 ], 253 "messages": [ 254 { 255 "severity": "error", 256 "pos": {"line": 33, "column": 4}, 257 "endPos": {"line": 33, "column": 17}, 258 "data": "tactic ’apply’ failed, failed to unify\n 0 < ?a * ?b\nwith\n 0 ≤...

Pith tools

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