Pith. sign in

REVIEW 5 major objections 5 minor 2 cited by

Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models

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

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

Pith's one-line read Without any training, a careful three-phase coordination of off-the-shelf reasoning models and tactic-step provers matches RL-trained state of the art on formal math benchmarks.

desk verdict Solid engineering and honest ablations, but the headline parity with RL-trained provers rests on a post-hoc corrected benchmark and a different Lean version—worth refereeing, not taking at face value. read the letter →

arxiv 2506.11487 v1 pith:BDHQTE4J submitted 2025-06-13 cs.AI

Chenrui Cao , Liangcheng Song , Zenan Li , Xinyi Le , Xian Zhang , Hui Xue , Fan Yang This is my paper · ORCID
classification cs.AI
keywords automatedtheoremprovingLean4Draft-Sketch-Proveneuro-symbolicreasoningmodelsreinforcementlearningtacticstepproversminiF2F
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

DSP+ is an inference-only revival of the Draft, Sketch, and Prove framework. It claims that, with no model training or fine-tuning, a careful three-phase coordination of off-the-shelf reasoning models and tactic-step provers can match reinforcement-learning-trained theorem provers on standard benchmarks. On miniF2F-test it solves 80.7%, on ProofNet-test 32.8%, and on PutnamBench 24 of 644 problems, while spending fewer inference tokens than a frontier RL-trained prover at equal accuracy. It also proves imo_2019_p1, an IMO problem no prior system solved, and exposes eight wrongly formalized miniF2F statements. If the parity holds, large-scale RL training is not the only route to advanced formal theorem proving.

What carries the argument

The load-bearing mechanism is the three-phase DSP+ workflow, where each phase is engineered with the next phase in mind. In the sketch phase, LLM-generated subgoals are written with `prove_with[...]` hypothesis hints, which tell the prover which assumptions to keep and prevent cluttered proof states; lines that do not parse are masked, either commented out or replaced with `sorry`, so the rest of the sketch survives. In the proving phase, Aesop, a white-box best-first proof search for Lean, is modified so its tree nodes can be expanded either by built-in symbolic tactics or by tactic proposals from BFS-Prover, operating directly on Lean proof states rather than on reconstructed theorem statements. The draft phase feeds this machinery by prompting a reasoning model for one-equation-per-step drafts and removing thinking tokens, keeping the sketch short enough to avoid long-context degradation.

What would settle it

Re-run DSP+ and the cited baselines on the original, uncorrected miniF2F statements under a single Lean version, and check whether DSP+ still reaches 80.7% and whether the corrected statements are the only ones it solves; a significant drop would overturn the parity claim.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the original DSP pipeline's poor results in Lean 4 came from coarse, phase-independent coordination, not from a fundamental limit of the inference-only paradigm. DSP+ improves each phase individually and in relation to the others: reasoning models produce concise natural-language drafts with thinking tokens stripped; the sketch model formalizes these as `have` subgoals carrying explicit hypothesis hints (`prove_with [h1, h2]`); and syntactically broken sketch lines are masked instead of restarting the sketch. The proving phase then merges Aesop's tree search with a BFS-Prover step prover, so every node can be expanded by either the symbolic engine or the neural prover. With a QwQ-32B draft, DeepSeek-V3-0324 sketch, and BFS-Prover proving, DSP+ reaches 79.5% on miniF2F-test at pass@1024, and swapping in DeepSeek-R1 as the draft model raises this to 80.7%. At that level it matches Kimina-Prover-Preview-72B at pass@8192 and approaches DeepSeek-Prover-V2-671B, while using less inference budget. It proves imo_2019_p1, an IMO problem not solved by any prior work, and uses its human-readable proof skeletons to find eight misformalized miniF2F statements, which the paper corrects in its experiments.

Load-bearing premise

The headline parity assumes that solving the eight corrected miniF2F statements is no easier than solving the original ones, and that comparing against baselines evaluated on their own Lean versions is a fair apples-to-apples comparison.

Editorial extensions

If this is right

  • Large-scale RL training is not the only route to state-of-the-art formal proving; the paper's inference-only pipeline matches a frontier RL-trained prover at equal accuracy.
  • DSP+ extends the set of automatically provable IMO problems, proving imo_2019_p1 for the first time.
  • The readable subgoal structure turns the prover into a benchmark-auditing tool, leading to eight corrected miniF2F statements.
  • Ensembling different draft and sketch models raises miniF2F-test accuracy to 83.6%, showing model diversity is a resource even without training.
  • Because each phase is modular, the pipeline can be redeployed with newer reasoning models at low cost.

Reading between the lines

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

  • Editorial inference: the parity claim is only as fair as the benchmark comparison; the paper's eight corrected miniF2F statements mean a same-statement, same-Lean-version head-to-head is needed to make the match with prior published results airtight.
  • Editorial inference: error-line masking is a double-edged repair; it keeps workflows alive, but commented-out sketch lines could silently change what is being proved, so counting how often masked lines turn out to be genuinely unprovable would quantify this risk.
  • Editorial inference: the human-readable sketches produced by DSP+ could serve as a curriculum for RL training, not just cold-start data, by teaching a model to imitate the subgoal decompositions that make proofs tractable.
  • Editorial inference: because the original DSP ran on Isabelle, the same neuro-symbolic coordination should transfer to other proof assistants, with the assistant's native symbolic search in place of Aesop.
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

5 major / 5 minor

Summary. This paper proposes DSP+, an inference-only, three-phase theorem-proving pipeline for Lean 4. In the draft phase, a reasoning LLM generates a concise natural-language proof outline; in the sketch phase, a second LLM autoformalizes the outline into a hierarchy of subgoals with explicit hypothesis hints, and a rule-based "error line masking" repair removes syntactically invalid lines; in the proving phase, the subgoals are discharged by an integration of Aesop tree search with a step prover (BFS-Prover-7B). The default configuration (QwQ-32B, DeepSeek-V3-0324, BFS-Prover) reports 79.5% on miniF2F-test, 32.8% on ProofNet-test, and 24/644 on PutnamBench; replacing QwQ with DeepSeek-R1 gives 80.7% on miniF2F-test, and an ensemble of six configurations reaches 83.6%. The paper further claims that DSP+ proves imo_2019_p1 for the first time and that it discovered eight wrong formalizations in miniF2F. The evaluation uses Lean 4 v4.17.0-rc1, and the headline comparison is made against RL-trained provers such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B.

Significance. If the headline claims held on a fixed, version-controlled benchmark, this would be a notable result: it would show that an inference-only neuro-symbolic pipeline, using off-the-shelf models, can reach parity with RL-trained provers on miniF2F while spending fewer inference tokens, and it would provide a useful tool for proof-data generation and formalization auditing. The paper's strengths include extensive ablations over draft/sketch/proving components, open prompts, a full trace for imo_2019_p1, discussion of failure modes, and the formalization-error discovery workflow. The main caveat is that several comparison mechanisms—dataset corrections, Lean-version differences, accumulative ensembling, and token accounting—are not yet aligned between DSP+ and the cited systems, so the significance is conditional on resolving these measurement issues.

major comments (5)
  1. [§5.2, Appendix F, Table 1] The central parity claim is computed on a modified benchmark. Appendix F identifies eight miniF2F-test statements that were corrected after DSP+ failures, and footnote 5 states "We use their corrected versions in our experiments," while §5.2 describes the benchmark only as "the Lean 4 version." The 80.7%/83.6% numbers in Table 1 therefore do not measure the same problem set as the cited Kimina-Prover-Preview or DeepSeek-Prover-V2 results. Please report results on both the original and corrected statement sets, and either apply the corrections uniformly to all compared systems or remove the corrected-benchmark results from the headline comparison.
  2. [§5.1, §E.4, footnote 4] The comparison is also not version-matched. DSP+ runs on Lean 4 v4.17.0-rc1, while the cited baselines report results on their own Lean/Mathlib versions; §E.4 demonstrates that a proof can succeed under v4.9.0-rc1 and fail under v4.17.0-rc1, and footnote 4 notes version-related issues for DeepSeek-Prover-V2. These environment differences can change pass rates independently of the proving method. The paper should either re-run the compared systems on identical statements and Lean versions or explicitly qualify every cross-system number as version-sensitive.
  3. [§5.3, Table 2] The "DSP+ ensemble" result is reported as an accumulative union over six configurations with heterogeneous budgets (three at pass@1024, three at pass@128), not as a single algorithm with a defined total budget. Placing this union in Table 1 next to single-method pass@k numbers makes the comparison unclear, especially since §5.3 claims parity "under the same sample budget." Please specify the total number of workflow attempts, tokens, and search budget for the ensemble, and compare it against an equivalently defined budget for each baseline.
  4. [§6.4, Table 3] The token-efficiency claim relies on average token counts reported in other papers for DeepSeek-Prover-V2 and Kimina-Prover-Preview, while DSP+ token counts are measured under the authors' own sampling configuration; the pass counts also differ (1024 vs. 8192). Please state exactly how each table entry is computed, including whether decoding settings and tokenizer conventions are matched, and provide sensitivity estimates for the total-token comparison.
  5. [Table 1, §5.2] PutnamBench results are not directly comparable across rows: DSP+ rows use a 644-problem Lean subset, whereas DeepSeek-Prover-V2 rows use 658 problems, and §5.2 notes the benchmark "is extended to 658 problems later." Reporting 24/644 next to 49/658 without a common denominator can misstate the relative performance. Please use a fixed version of PutnamBench for all systems or report both counts with explicit version labels.
minor comments (5)
  1. [§3.1, §6.2, Figure 4] The conciseness motivation in §3.1 is weakened by the paper's own ablation: Figure 4 shows that removing the conciseness prompt ("No Format") slightly outperforms the default concise format (75.4% vs. 74.2% at pass@128). Please reconcile this with the abstract's claim that concise draft generation benefits the pipeline, or reposition conciseness as an efficiency/robustness property rather than an accuracy improvement.
  2. [Appendix H] The imo_2019_p1 trace mixes sketch lines, proof lines, inline "sorry" placeholders, and editorial comments in a two-column layout; please provide a standalone, verified .lean file (or a pointer to the released artifact) so the claim that the final proof contains no unproved axioms can be checked directly.
  3. [References] Reference [52] duplicates reference [8] (InternLM2.5-StepProver), and the reference list/header contain minor formatting inconsistencies; please clean up citations and duplicate entries.
  4. [Table 6] In the ProverBench table, DSP+ ensemble (55.69%) is compared to DeepSeek-Prover-V2-671B (59.1% at 512) without stating the ensemble's total sample budget; please add budget and token counts to this table so the comparison is interpretable.
  5. [§4] The phrase "pass@k" is used for executing the whole workflow k times, which differs from the standard next-tactic pass@k used in some baselines; please define the sampling unit (workflow attempt vs. tactic sample) explicitly when reporting pass@1024 and pass@8192.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: DSP+ makes no derivation claims that reduce to their inputs; benchmark corrections are a comparability concern, not a circular step.

full rationale

I find no circular step in the sense defined by the seven patterns. DSP+ is an inference-only pipeline whose headline results are empirically verified Lean proofs; every success is checked by Lean 4 (v4.17.0-rc1), so the reported proof outcomes are not equivalent to the pipeline's inputs by construction. The configuration choices (QwQ-32B draft, DeepSeek-V3 sketch, BFS-Prover step prover, Aesop tree search, error-line masking) are disclosed ablations and design decisions, not fitted parameters that are then renamed as predictions. The one substantive evaluation concern is benchmark modification: Appendix F reports eight miniF2F-test statements identified as wrongly formalized after DSP+ failures, and footnote 5 states "We use their corrected versions in our experiments," while Section 5.2 describes the benchmark only as "the Lean 4 version." This is a benchmark-comparability and fairness threat relative to systems evaluated on uncorrected statements and different Lean versions, but it is not circularity under the required definition: no equation or formal claim reduces to its own input, and the proof checks are still external. Appendix E.4's demonstration that proofs can succeed or fail depending on Lean version reinforces the comparability concern, not a circularity finding. Self-citations are not load-bearing: the cited prior work by overlapping authors appears only in general related-work lists and does not justify the central claim. The central claim remains an empirical, externally checkable result.

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

The central claim is empirical, so the ledger records the chosen system configurations and the evaluation assumptions rather than derivation parameters. The free parameters are hand-set search and sampling budgets; they affect the pass@k curves but are disclosed and ablated. The most consequential evaluation axiom is that the corrected 8 miniF2F statements are the right formalization. The paper postulates no new mathematical entities.

free parameters (6)
  • Search beam width = 4
    Chosen by hand for the Aesop tree search (Section 5.1).
  • Tree size limit = 64
    Constraints on expansion iterations per subgoal (Section 5.1, Appendix B).
  • Search attempts per subgoal = 8
    The A parameter in the A x W x T budget for the proving phase (Appendix B).
  • Sampling temperatures = QwQ 0.6, DeepSeek-V3 0.7, BFS-Prover 1.1
    API sampling parameters in Section 5.1.
  • Workflow attempts per problem = 1024 (miniF2F), 128 (ProofNet and PutnamBench)
    Pass@k budget; a chosen evaluation budget rather than a fitted constant.
  • Ensemble configuration schedule = 6 combinations on miniF2F; R1-V3-BFS pass@32 added on ProofNet and PutnamBench
    Table 2 configurations selected to add accumulated solved problems; affects the 83.6% ensemble number.
assumptions (4)
  • domain assumption Lean 4 v4.17.0-rc1 and Mathlib4 are sound; every proof accepted by Lean is correct.
    Section 5.1 states verification uses Lean 4 with Mathlib4.
  • ad hoc to paper The corrected versions of 8 miniF2F statements used in evaluation faithfully represent the intended math problems.
    Appendix F introduces these corrections after DSP+ failures; they are not in the standard miniF2F release used by prior work.
  • domain assumption Prior systems' reported pass@k numbers and token counts are reliable and comparable despite different Lean versions and sampling budgets.
    Section 6.4 and Tables 1-6 compare against numbers from DeepSeek-Prover-V2 and Kimina-Prover; the paper itself notes Lean version differences affect accuracy.
  • domain assumption BFS-Prover-7B and Aesop search behave as described and terminate within the configured time limit.
    The proving phase relies on this integration (Section 3.3, Appendix A).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models." pith.science (2026). https://pith.science/paper/BDHQTE4J

@misc{pith2026250611487,
  author       = {Pith},
  title        = {Pith review of: Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BDHQTE4J}},
  note         = {Machine review of arXiv:2506.11487}
}
read the original abstract

Recent advancements, such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coordination of existing off-the-shelf reasoning models and tactic step provers can achieve comparable performance. This paper introduces \textbf{DSP+}, an improved version of the Draft, Sketch, and Prove framework, featuring a \emph{fine-grained and integrated} neuro-symbolic enhancement for each phase: (1) In the draft phase, we prompt reasoning models to generate concise natural-language subgoals to benefit the sketch phase, removing thinking tokens and references to human-written proofs; (2) In the sketch phase, subgoals are autoformalized with hypotheses to benefit the proving phase, and sketch lines containing syntactic errors are masked according to predefined rules; (3) In the proving phase, we tightly integrate symbolic search methods like Aesop with step provers to establish proofs for the sketch subgoals. Experimental results show that, without any additional model training or fine-tuning, DSP+ solves 80.7\%, 32.8\%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench, respectively, while requiring fewer budgets compared to state-of-the-arts. DSP+ proves \texttt{imo\_2019\_p1}, an IMO problem in miniF2F that is not solved by any prior work. Additionally, DSP+ generates proof patterns comprehensible by human experts, facilitating the identification of formalization errors; For example, eight wrongly formalized statements in miniF2F are discovered. Our results highlight the potential of classical reasoning patterns besides the RL-based training. All components will be open-sourced.

Figures

Figures reproduced from arXiv: 2506.11487 by the authors.

Figure 1
Figure 1. The best achieved results and the inference tokens used of top solutions on miniF2F-test. [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. The workflow of DSP+ consists of three phases. Every phase is enhanced with neural [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Ablation of DSP+ components, which shows the synergy in DSP+. Draft-Sketch, Pass@n #Solved #Accum. QwQ-V3@1024 – +194 R1-V3@1024 +5, -2 +5 QwQ-QwQ@1024 +4, -5 +2 None-V3@128 +1, -20 +1 QwQ(No format)-V3@128 +1, -11 +1 R1-QwQ@128 +3, -11 +1 Total: 204 [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (5 more)
Figure 5
Figure 5. Figure 5: Ablation of Sketch Optimizations. Both optimizations are effective. 6.3 The Robustness of DSP+ Different Draft Models. As shown in [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]
Figure 6
Figure 6. Figure 6: Comparing Different Draft Models. Reasoning models are optimal. 0 32 64 96 128 #Workflow Attempts Per Problem 100 120 140 160 180 #Successful Proofs Minif2f Test Problems Solved (out of 244) DeepSeek-V3-0324 (74.2%) GPT-4o (71.3%) Qwen2.5-32B-Instruct (71.7%) QwQ-32B (…
Figure 8
Figure 8. Figure 8: The Performance of DSP+ with Different Draft Models. Reasoning models are better than [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: The Performance of DSP+ with Different Sketch Models. DeepSeek-V3 shows strong [PITH_FULL_IMAGE:figures/full_fig_p017_9.png]
Figure 10
Figure 10. Figure 10: Ablation of Human Informal Proof. Human informal proof offers no help for reasoning [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

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.

  2. Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

    cs.LO 2025-07 conditional novelty 6.0 of 10

    A decoupled reasoning-and-proving framework generated machine-verified Lean proofs for five post-2000 IMO problems.

Reference graph

Works this paper leans on

63 extracted references · 31 canonical work pages · cited by 2 Pith papers

  1. [1]

    AI achieves silver-medal standard solving In- ternational Mathematical Olympiad problems

    AlphaProof and AlphaGeometry teams. AI achieves silver-medal standard solving In- ternational Mathematical Olympiad problems. https://deepmind.google/discover/blog/ ai-solves-imo-problems-at-silver-medal-level/ , July 2024. Accessed: 2025-05-12

    work page 2024

  2. [2]

    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, 2025

    2025

  3. [3]

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

    work page 2025

  4. [4]

    Bfs-prover: 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. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025

    arXiv 2025

  5. [5]

    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

  6. [6]

    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, pages arXiv–2502, 2025

    work page 2025

  7. [7]

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving

    Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024

    arXiv 2024

  8. [9]

    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

Show all 63 references
  1. [10]

    Deepseek-prover-v1

    Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024

    2024 arXiv

  2. [11]

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024

    2024 arXiv

  3. [12]

    Minif2f: a cross-system benchmark for formal olympiad-level mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021

    2021 arXiv

  4. [13]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Repr...

    2023

  5. [14]

    An essay on the psychology of invention in the mathematical field

    Jacques Hadamard. An essay on the psychology of invention in the mathematical field. Courier Corporation, 1954

    1954

  6. [15]

    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. arXiv preprint arXiv:2410.16429, 2024

    arXiv

  7. [16]

    The lean theorem prover (system description)

    Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 3...

    2015

  8. [17]

    Qwq-32b: Embracing the power of reinforcement learning, March 2025

    Qwen Team. Qwq-32b: Embracing the power of reinforcement learning, March 2025

    2025

  9. [18]

    Deepseek-v3 technical report, 2024

    DeepSeek-AI. Deepseek-v3 technical report, 2024

    2024

  10. [19]

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, 2025

    DeepSeek-AI. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, 2025

    2025

  11. [20]

    Proof or bluff? evaluating llms on 2025 usa math olympiad

    Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunovi´c, Nikola Jovanovi´c, and Martin Vechev. Proof or bluff? evaluating llms on 2025 usa math olympiad. arXiv preprint arXiv:2503.21934, 2025

    2025 arXiv

  12. [21]

    A lean dataset for international math olympiad: Small steps towards writing math proofs for hard problems

    Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. A lean dataset for international math olympiad: Small steps towards writing math proofs for hard problems. arXiv preprint arXiv:2411.18872, 2024

    2024 arXiv

  13. [22]

    Isabelle: A generic theorem prover

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

    1994

  14. [23]

    Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions

    Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013

    2013

  15. [24]

    A survey on deep learning for theorem proving

    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024

    2024 arXiv

  16. [25]

    Formal mathematical reasoning: A new frontier in ai

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024

    2024 arXiv

  17. [26]

    Proof artifact co-training for theorem proving with language models

    Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, 2022

    2022

  18. [27]

    Autoformalization with large language models

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022

    2022

  19. [28]

    Formal mathematics statement curriculum learning

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, 2023

    2023

  20. [29]

    Alchemy: Amplifying theorem-proving capability through symbolic mutation

    Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, and Ping Wei. Alchemy: Amplifying theorem-proving capability through symbolic mutation. arXiv preprint arXiv:2410.15748, 2024

    2024 arXiv

  21. [30]

    Multi-language diversity benefits autoformalization

    Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformalization. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024

    2024

  22. [31]

    Lean-github: Compiling github lean repositories for a versatile lean prover

    Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024

    2024 arXiv

  23. [32]

    Lean workbook: A large- scale lean problem set formalized from natural language math problems

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large- scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024

    2024 arXiv

  24. [33]

    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, 2024

    2024

  25. [34]

    Towards large language models as copilots for theorem proving in lean

    Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534, 2024

    2024 arXiv

  26. [35]

    Generative language modeling for automated theorem proving

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

    2009 arXiv

  27. [36]

    Hypertree proof search for neural theorem proving

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337–26349, 2022

    2022

  28. [37]

    Proving theorems recursively

    Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively. arXiv preprint arXiv:2405.14414, 2024

    2024 arXiv

  29. [38]

    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, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Associ...

    2023

  30. [39]

    Proving olympiad inequalities by synergizing llms and symbolic reasoning

    Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, and Xiaox- ing Ma. Proving olympiad inequalities by synergizing llms and symbolic reasoning. arXiv preprint arXiv:2502.13834, 2025

    2025 arXiv

  31. [40]

    Lego-prover: Neural theorem proving with growing libraries

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024

    2024

  32. [41]

    Baldur: Whole-proof generation and repair with large language models

    Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229–1241, 2023

    2023

  33. [42]

    Herald: A natural language annotated lean 4 dataset

    Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. arXiv preprint arXiv:2410.10878, 2024

    2024 arXiv

  34. [43]

    Aesop: White-box best-first proof search for lean

    Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 253–266, 2023

    2023

  35. [44]

    Leanabell-prover: Posttraining scaling in formal reasoning

    Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122, 2025

    2025 arXiv

  36. [45]

    Scaling relationship on learning mathematical reasoning with large language models

    Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. Scaling relationship on learning mathematical reasoning with large language models. arXiv preprint arXiv:2308.01825, 2023

    2023 arXiv

  37. [46]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023

    2023 arXiv

  38. [47]

    Putnambench: Evaluating neural theorem-provers on the putnam mathe- matical competition

    George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathe- matical competition. In The Thirty-eight Conference on Neural Information Proces...

    2024

  39. [48]

    Sledgehammer: judgement day

    Sascha Böhme and Tobias Nipkow. Sledgehammer: judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 5 , pages 107–121. Springer, 2010

    2010

  40. [49]

    Subgoalxl: Subgoal-based expert learning for theorem proving

    Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint arXiv:2408.11172, 2024

    2024 arXiv

  41. [50]

    Subgoal-based demonstration learning for formal theorem proving

    Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-based demonstration learning for formal theorem proving. In Forty-first International Conference on Machine Learning, 2024

    2024

  42. [51]

    Lost in the middle: How language models use long contexts

    Nelson F Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. Lost in the middle: How language models use long contexts. Transactions of the Association for Computational Linguistics, 12:157–173, 2024

    2024

  43. [52]

    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

  44. [53]

    Gonzalez, Hao Zhang, and Ion Stoica

    Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems...

    2023

  45. [54]

    The Lean mathematical library

    Mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, page 367–381. Association for Computing Machinery, 2020

    2020

  46. [55]

    Putnambench leaderboard, 2023

    Trishul Chilimbi and PutnamBench Contributors. Putnambench leaderboard, 2023. Accessed: 2025-05-05

    2023

  47. [56]

    DeepSeek-Prover V2 TODO List

    Lean Zulip Chat. DeepSeek-Prover V2 TODO List. https://leanprover.zulipchat.com/#narrow/ channel/219941-Machine-Learning-for-Theorem-Proving/topic/DeepSeek-Prover.20V2. 20TODO.20List/with/516083350, 2025. Accessed: 2025-05-12

    2025

  48. [57]

    A read-eval-print-loop for Lean 4

    Leanprover Community. A read-eval-print-loop for Lean 4. https://github.com/ leanprover-community/repl, 2023. 12 A Implementation Details A.1 The Configuration of Aesop We configure Aesop’s search space to be either tactics proposed by the step prover, or be with a few commonl...

    2023

  49. [58]

    := by intro b -- exact h2 (b + 1) sorry (simp_all) -- Step 8 have h8 : ∀ b, f 2 + 2 * f b = f 0 + 2 * f (b +

  50. [59]

    This is proved later by BFS-Prover

    := by prove_with [h6, h7] clear * - h6 h7 (simp_all) -- Step 9 have h9 : ∀ b, 2 * f (b + 1) = (f 2 - f 0) + 2 * f b := by prove_with [h8] clear * - h8 exact fun b 7→ by linarith [h8 b] -- Step 10 have h10 : ∀ b, f (b + 1) = ((f 2 - f 0) / (2 : Z )) + f b := by prove_with [h9] ...

  51. [60]

    Concise Steps

    ^ 3), sq_nonneg (b ^ 4 - (2 / 3) ^ 4), sq_nonneg (b ^ 5 - (2 / 3) ^ 5), sq_nonneg (b ^ 6 - (2 / 3) ^ 6), sq_nonneg (b ^ 7 - (2 / 3) ^ 7), sq_nonneg (b ^ 8 - (2 / 3) ^ 8), sq_nonneg (b ^ 9 - (2 / 3) ^ 9)] This statement appears as a subgoal. Unfortunately, under our configurati...

  52. [61]

    Simplify 29 mod 7: 29 ÷ 7 = 4remainder 1 =⇒ 29 ≡ 1 mod 7 Therefore: 2913 mod 7≡ 113 mod 7 = 1 mod 7

  53. [62]

    Simplify 5 mod 7: 5 < 7 =⇒ 5 ≡ 5 mod 7 To compute 513 mod 7, apply Fermat’s Little Theorem: Since 7 is prime and 5ot ≡ 0 mod 7 , 56 ≡ 1 mod 7 Express 13 as 6 × 2 + 1: 513 = (56)2 × 51 ≡ (1)2 × 5 ≡ 5 mod 7

  54. [63]

    Compute the difference modulo 7: (2913−513) mod 7 ≡ (1−5) mod 7 ≡ −4 mod 7 Convert −4 to a positive residue: −4 + 7 = 3 =⇒ −4 ≡ 3 mod 7 Conclusion: 3 Thus, (2913 − 513) mod 7 = 3. L Draft Comparison of QwQ-32B and DeepSeek-R1 In our early toy experiments, we provide the same d...

    1962

  55. [64]

    + 1 / 4 := by nlinarith [Real.sq_sqrt (show 0 ≤ x + 1 by linarith), Real.sq_sqrt (show 0 ≤ 3 - x by linarith), sq_nonneg (Real.sqrt (x + 1) - 1 / 2)] have h 611 : (Real.sqrt (3 - x)) ^ 2 = 3 - x := by rw [Real.sq_sqrt] <;> linarith nlinarith [Real.sq_sqrt (show 0 ≤ x + 1 by li...

Pith tools

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