Pith. sign in

REVIEW 4 major objections 5 minor 4 cited by

Solving Formal Math Problems by Decomposition and Iterative Reflection

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

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

Pith's one-line read A stock general-purpose LLM, orchestrated as a reflective agent with a custom Lean 4 DSL, proves 95.9% of miniF2F-test problems without fine-tuning.

desk verdict A genuinely strong agentic prover with kernel-verified proofs, but the headline SOTA claim is undercut by a post-hoc sample budget definition—worth refereeing, not trusting at face value. read the letter →

arxiv 2507.15225 v1 pith:SXCYVHMX submitted 2025-07-21 cs.AI cs.LGcs.LO

Yichi Zhou , Jianqiu Zhao , Yongxin Zhang , Bohan Wang , Siran Wang , Luoxin Chen , Jiahui Wang , Haowei Chen
show 9 more authors
Allan Jie Xinbo Zhang Haocheng Wang Luong Trung Rong Ye Phan Nhat Hoang Huishuai Zhang Peng Sun Hang Li
This is my paper
classification cs.AIcs.LGcs.LO
keywords formaltheoremprovingLean4LLMagentreflectivedecompositioniterativeproofrepairdomain-specificlanguageminiF2Ftest-timescaling
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

$\Delta$ Prover is an agentic theorem prover that wraps a stock general-purpose LLM in an interactive loop with the Lean 4 proof checker. The paper claims that this training-free agent proves 95.9% of the miniF2F-test benchmark, outperforming every previously reported prover, including systems fine-tuned specifically on formal mathematics, and that it reaches 85% on the IMO subset of the benchmark. The proposed reason is that reflective decomposition and iterative proof repair let the LLM handle long proofs by splitting them into verifiable subproblems, while a custom DSL manages the subproblem state and reassembles the verified pieces. A sympathetic reader would care because the result implies that the bottleneck in automated theorem proving is not formal-language mastery of the model but the structure of the search around it.

What carries the argument

The load-bearing object is a custom monad layer called PlayM, built on Lean 4's TacticM, exposing four tactics: suppose for introducing hypotheses, define for introducing expressions, show for posing subgoals, and conclude for assembling subproofs. The DSL records proof states and dependency graphs, extracts each subgoal as a standalone formal statement, and uses Lean's delaborator to emit the complete proof once all subgoals are solved. Around it runs the reflective decomposition algorithm: generate an informal plan, formalize it as a DSL sketch, solve subgoals independently, and on failure feed the unsolved subproblem list back to the LLM to regenerate the sketch.

What would settle it

Run $\Delta$ Prover on all 244 miniF2F-test problems with a hard cap of 16,384 API calls per problem, counting calls on failed attempts as well as successful ones, and compare the pass rate with Table 1. If the rate is materially below 95.9%, the claimed advantage over baselines depends on the paper's budget definition rather than on the agent itself.

Watch

Extended reading notes

Core claim

The central claim is that a general-purpose LLM, without any fine-tuning on formal corpora, can become the strongest known prover on miniF2F-test when orchestrated as an agent. The agent first tries direct proof generation with iterative repair: it proposes a Lean 4 proof, reads the kernel's error message, retrieves relevant theorems, and tries again. When direct repair stalls, it switches to reflective decomposition: the LLM writes an informal proof plan, translates it into a formal sketch in a custom DSL, the DSL extracts subproblems, each subproblem is solved by the repair loop, and the pieces are consolidated into a single verified proof. The paper reports 95.9% accuracy on miniF2F-test and 85% on its IMO subset, with a sample budget of 16,384 API calls, and shows that this repair-based agent scales better with test-time compute than best-of-N sampling.

Load-bearing premise

The comparison rests on treating the reported 16,384-call sample budget as a fixed per-problem budget and on one stochastic run being representative, whereas the budget is actually the maximum number of API calls used by successful proofs.

Editorial extensions

If this is right

  • Formal theorem proving no longer requires a model fine-tuned on formal corpora; agentic scaffolding around a general-purpose LLM is enough to reach state-of-the-art pass rates.
  • Decomposition reduces the cost of long proofs: the IMO 2019 P1 case was split into 83 subproblems and solved in about 332 API calls, whereas direct repair failed after 1024 calls.
  • Iterative proof repair scales better than independent sampling: under a fixed budget, increasing repair attempts beats increasing independent attempts, and the gap widens as the budget grows.
  • The DSL's automatic proof consolidation turns decomposition into a practical strategy, allowing decomposed subproofs to be reassembled into one verified Lean 4 script without manual bookkeeping.

Reading between the lines

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

  • Editorial inference: the same decomposition-and-repair loop should transfer to other proof assistants, since the DSL is a bookkeeping layer over the kernel rather than a Lean-specific training regime; the paper only evaluates Lean 4.
  • Editorial inference: if decomposition quality is the main lever, then stronger prompts for autoformalization and proof planning may improve theorem proving more than scaling the underlying LLM.
  • Editorial inference: the agent structure suggests that test-time compute in provers should be reported with a strict per-problem budget, so that training-free systems and fine-tuned systems are compared on the same footing.
  • Editorial inference: the same feedback-loop pattern could apply to other settings where a verifier gives cheap error signals, such as proof-carrying code or hardware verification.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. This paper introduces Delta Prover, a training-free agentic theorem prover that combines a stock Gemini 2.5 Pro LLM with a custom Lean 4 DSL ('PlayM') to reflectively decompose problems into subproblems and iteratively repair failed proof attempts. The authors report 95.9% on miniF2F-test and 85% on the IMO subset, claiming state-of-the-art results that surpass specialized fine-tuned provers, and they report a stronger test-time scaling law than best-of-N sampling. The core algorithmic contribution is the interaction between iterative proof repair, reflective decomposition, DSL-based subproblem extraction, and automatic proof consolidation.

Significance. If the empirical claims survive a controlled evaluation, this is a significant result: it would show that a general-purpose LLM with no formal-theorem-proving fine-tuning can outperform specialized provers on a standard benchmark, with all final proofs checked by the Lean 4 kernel. The DSL for subproblem management and the repair loop are potentially reusable components, and the paper is concrete about prompts, algorithms, and a worked IMO example. The main weakness is not proof correctness but resource accounting: the reported sample budget is a post-hoc statistic, not a fixed per-problem budget, which currently prevents the central comparison from being interpreted as claimed.

major comments (4)
  1. [Section 4.2, Table 1] The sample budget in Table 1 is not a fixed resource limit: Section 4.2 states that 'once Delta Prover solves a problem, we record the number of API calls used for that successful attempt' and takes the maximum over solved problems. Under this definition, unsolved problems may consume an unbounded number of calls, whereas baselines such as DeepSeek-Prover-V2 (8,192) and Kimina-Prover (42,000) are evaluated under fixed per-problem budgets. The headline comparison therefore does not control compute, and the claim that Delta Prover surpasses specialized models at comparable cost is not established; please re-run with a fixed per-problem budget or report the full per-problem cost distribution and a pass@k-style comparison at equal budgets.
  2. [Figure 4] The test-time scaling plot uses the same post-hoc cost measure, so it shows the cost of successful solutions rather than performance at a controlled budget. A scaling law for a prover should report success rate as a function of a preallocated per-problem budget; please also include multiple random seeds at temperature 1 with variance, since the current single-run results do not indicate how stable the 95.9% figure is.
  3. [Section 4.3] The optimal (m, n) configuration is selected on miniF2F-test itself (left panel of Figure 5) with no validation split. If this selection informed the configuration used for the main results, the benchmark has been used for hyperparameter tuning; please specify the selection protocol and, if possible, validate on a held-out set.
  4. [Section 4.1] The benchmark section says the authors 'fix errors in the statements similar to [33, 41]' but does not enumerate these fixes or release the exact statements. If the fixed statements differ from those used by the baselines, the accuracy comparison is not apples-to-apples; please release the diffs or confirm that the statements are byte-identical to the ones used by the baselines.
minor comments (5)
  1. [Section 2.1.2] The text says DSP uses 'the formal language Isabella'; this should be 'Isabelle'.
  2. [Section 3] The related-work section refers to 'CORPA' but the cited system is COPRA; please correct the name and check for consistency.
  3. [References] Reference [42] has a duplicated title ('Kimina-prover: Kimina-prover: ...'); this needs to be fixed in the bibliography.
  4. [Section 4.3, Effect of Reflective Decomposition] The decomposition study on IMO 2019 P1 is a single anecdotal example; if the claim is that decomposition improves efficiency in general, additional problems or a small quantitative study would strengthen the presentation.
  5. [Figure 3] The DSL example in Figure 3 is visually dense and hard to parse in print; consider presenting the four DSL constructs in a compact table or listing them separately.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Delta Prover's central 95.9% miniF2F-test claim is an empirical pass rate verified by the external Lean 4 kernel, not a quantity forced by its own definitions or fitted inputs.

full rationale

Delta Prover's derivation chain is empirical rather than definitional. The claimed 95.9% success rate is the fraction of miniF2F-test statements for which the agent produces a Lean 4 proof accepted by the Lean kernel, an independent machine-checked verifier. No parameter in the framework is fitted to define this outcome, and no theorem is invoked whose statement is equivalent to the target result. The DSL (PlayM tactics) is a new engineering component, but its correctness is enforced by Lean's kernel when proofs are consolidated, and its success is measured against an external benchmark rather than against the DSL's own semantics. The only potentially self-referential element is Section 4.2's definition of 'sample budget' as the maximum API calls among solved problems, which is a post-hoc reporting statistic rather than a fixed per-problem cap; this may weaken the compute-controlled comparison with baselines, but it is a measurement/reporting limitation, not a case where a prediction reduces by construction to its inputs or to a self-citation. No load-bearing self-citation or imported uniqueness claim appears in the derivation. Thus no circular step is present.

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

No new physical or mathematical entities are introduced; the PlayM DSL is a software artifact, not a postulated natural entity. The main free parameters are the agent's hyperparameters, which are chosen by hand and potentially tuned on the test set. The central claim rests on assumptions about the base model's capabilities, the correctness of the custom DSL, the comparability of benchmark statement fixes, and the representativeness of a single run.

free parameters (4)
  • number of repair iterations per round (n) = not stated; selected as 'high' in ablation
    Ablation in Figure 5 varies n and m to find an optimal configuration under a fixed budget, with no described held-out validation split; the chosen n may overfit miniF2F-test.
  • number of direct-proof rounds (m) = not stated; traded against n
    Selected together with n in the same ablation; no sensitivity or validation details are reported.
  • max decomposition attempts (lmax) = not reported
    Algorithm 2 depends on lmax, but the paper does not state its value in the main experiments or provide a sensitivity analysis.
  • temperature = 1.0
    Chosen as 'common usage' in Section 4.1; no ablation or discussion of how temperature affects the success rate.
assumptions (4)
  • domain assumption General-purpose LLM Gemini 2.5 Pro can reliably follow the DSL prompt and reflect on Lean 4 feedback.
    The framework's success rests on the base model's instruction-following and self-correction abilities, but no other general-purpose LLM is tested (Section 4.1).
  • ad hoc to paper The custom PlayM DSL, implemented via Lean 4 metaprogramming, correctly extracts and consolidates subproblems without changing proof semantics.
    The DSL is introduced in Section 2.2, but no independent formal verification of the DSL implementation is provided, and the code is not released.
  • ad hoc to paper miniF2F-test statement fixes are equivalent to those used by prior baselines.
    Section 4.1 says the authors 'fix errors in the statements similar to [33,41]' without listing all fixes; if the fixes differ, the comparison to prior results may not be apples-to-apples.
  • domain assumption A single stochastic run at temperature 1 represents the true success rate.
    No repeated seeds or confidence intervals are reported in Table 1, so the 95.9% figure is a point estimate from one run.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Solving Formal Math Problems by Decomposition and Iterative Reflection." pith.science (2026). https://pith.science/paper/SXCYVHMX

@misc{pith2026250715225,
  author       = {Pith},
  title        = {Pith review of: Solving Formal Math Problems by Decomposition and Iterative Reflection},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SXCYVHMX}},
  note         = {Machine review of arXiv:2507.15225}
}
read the original abstract

General-purpose Large Language Models (LLMs) have achieved remarkable success in intelligence, performing comparably to human experts on complex reasoning tasks such as coding and mathematical reasoning. However, generating formal proofs in specialized languages like Lean 4 remains a significant challenge for these models, limiting their application in complex theorem proving and automated verification. Current approaches typically require specializing models through fine-tuning on dedicated formal corpora, incurring high costs for data collection and training. In this work, we introduce \textbf{Delta Prover}, an agent-based framework that orchestrates the interaction between a general-purpose LLM and the Lean 4 proof environment. Delta Prover leverages the reflection and reasoning capabilities of general-purpose LLMs to interactively construct formal proofs in Lean 4, circumventing the need for model specialization. At its core, the agent integrates two novel, interdependent components: an algorithmic framework for reflective decomposition and iterative proof repair, and a custom Domain-Specific Language (DSL) built upon Lean 4 for streamlined subproblem management. \textbf{Delta Prover achieves a state-of-the-art 95.9\% success rate on the miniF2F-test benchmark, surpassing all existing approaches, including those requiring model specialization.} Furthermore, Delta Prover exhibits a significantly stronger test-time scaling law compared to standard Best-of-N proof strategies. Crucially, our findings demonstrate that general-purpose LLMs, when guided by an effective agentic structure, possess substantial untapped theorem-proving capabilities. This presents a computationally efficient alternative to specialized models for robust automated reasoning in formal environments.

Discussion (0). Sign in to comment.

Forward citations

Cited by 4 Pith papers

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

  1. FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

    cs.CL 2026-07 conditional novelty 7.0 of 10

    FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.

  2. Intern-S1-MO: Long-horizon Reasoning Agent for Olympiad?Level Mathematical Problem Solving

    cs.CL 2025-12 conditional novelty 6.0 of 10

    A multi-round, lemma-memory reasoning agent with hierarchical RL reaches reported gold-medal-level scores on Olympiad math benchmarks, though the proof-based scores are self-graded.

  3. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    cs.AI 2025-07 conditional novelty 6.0 of 10

    Seed-Prover and Seed-Geometry prove 121 of 155 formalized past IMO problems, reach 99.6% on MiniF2F-test, and solve 5 of 6 IMO 2025 problems after the competition deadline.

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

    cs.AI 2025-07 conditional novelty 6.0 of 10

    A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.

Reference graph

Works this paper leans on

59 extracted references · 21 canonical work pages · cited by 4 Pith papers

  1. [1]

    Learning to reason in large theories without imitation.arXiv preprint arXiv:1905.10501, 2019

    Kshitij Bansal, Christian Szegedy, Markus N Rabe, Sarah M Loos, and Viktor Toman. Learning to reason in large theories without imitation.arXiv preprint arXiv:1905.10501, 2019

    arXiv 1905

  2. [2]

    Ai achieves silver-medal standard solving international mathematical olympiad problems, 2024

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

  3. [3]

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

    DeepSeek-AI. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning, 2025. URL https://arxiv.org/abs/2501.12948

    arXiv 2025

  4. [4]

    Stp: Self-play llm theorem provers with iterative conjecturing and proving.arXiv e-prints, pages arXiv–2502, 2025

    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

  5. [5]

    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

    arXiv 2025

  6. [6]

    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. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229–1241, 2023

    2023

  7. [7]

    Gemini 2.5 pro.https://deepmind.google/technologies/gemini/pro/, 2025

    Google DeepMind. Gemini 2.5 pro.https://deepmind.google/technologies/gemini/pro/, 2025

    work page 2025

  8. [8]

    Proof artifact co-training for theorem proving with language models.arXiv preprint arXiv:2102.06203, 2021

    Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models.arXiv preprint arXiv:2102.06203, 2021

    arXiv 2021

Show all 59 references
  1. [9]

    Measuring mathematical problem solving with the math dataset.NeurIPS, 2021

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset.NeurIPS, 2021

    2021

  2. [10]

    Gamepad: A learning environment for theorem proving

    Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608, 2018

    2018 arXiv

  3. [11]

    Opencoder: The open cookbook for top-tier code large language models.arXiv preprint arXiv:2411.04905, 2024

    Siming Huang, Tianhao Cheng, Jason Klein Liu, Jiaran Hao, Liuyihan Song, Yang Xu, J Yang, JH Liu, Chenchen Zhang, Linzheng Chai, et al. Opencoder: The open cookbook for top-tier code large language models.arXiv preprint arXiv:2411.04905, 2024

    2024 arXiv

  4. [12]

    Deepmath- deep sequence models for premise selection.Advances in neural information processing systems, 29, 2016

    Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath- deep sequence models for premise selection.Advances in neural information processing systems, 29, 2016

    2016

  5. [13]

    Isabelle

    Isabelle Project. Isabelle. https://isabelle.in.tum.de. Accessed: 2024-03-18

    2024

  6. [14]

    Openai o1 system card.arXiv preprint arXiv:2412.16720, 2024

    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

    2024 arXiv

  7. [15]

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

    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

    arXiv

  8. [16]

    Lisa: Language models of isabelle proofs

    Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392, 2021

    2021

  9. [17]

    Thor: Wielding hammers to integrate language models and automated theorem provers

    Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35:8360–8373, 2022

    2022

  10. [18]

    Hypertree proof search for neural theorem proving.Advances in neural information processing systems, 35:26337–26349, 2022

    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

  11. [19]

    Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving.arXiv preprint arXiv:2412.20735, 2024

    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

    2024 arXiv

  12. [20]

    Let’s verify step by step.arXiv preprint arXiv:2305.20050, 2023

    Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step.arXiv preprint arXiv:2305.20050, 2023. 15

    2023 arXiv

  13. [21]

    Lean-star: Learning to interleave thinking and proving

    Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024

    2024 arXiv

  14. [22]

    Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025

    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

    2025 arXiv

  15. [23]

    CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics, 2024

    Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, Zhengfeng Yang, Jujian Zhang, Lihong Zhi, Jia Li, and Zhengying Liu. CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics, 2024

    2024

  16. [24]

    Deep network guided proof search.arXiv preprint arXiv:1701.06972, 2017

    Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search.arXiv preprint arXiv:1701.06972, 2017

    2017 arXiv

  17. [25]

    Magnushammer: A transformer-based approach to premise selection.arXiv preprint arXiv:2303.04488, 2023

    Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection.arXiv preprint arXiv:2303.04488, 2023

    2023 arXiv

  18. [26]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InAutomated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021

    2021

  19. [27]

    Introducing deep research

    OpenAI. Introducing deep research. https://openai.com/index/introducing-deep-research/

  20. [28]

    Solving (some) formal math olympiad problems, 2022

    OpenAI. Solving (some) formal math olympiad problems, 2022. URLhttps://openai.com/index/formal-math/

    2022

  21. [29]

    Introducing openai o3 and o4-mini, 2025

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

    2025

  22. [30]

    Generative language modeling for automated theorem proving.arXiv preprint arXiv:2009.03393, 2020

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

    2009 arXiv

  23. [31]

    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

  24. [32]

    Mathematical reasoning via self-supervised skip-tree training

    Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757, 2020

    2006 arXiv

  25. [33]

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

    2025

  26. [34]

    Mathematical discoveries from program search with large language models.Nature, 625(7995):468–475, 2024

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al. Mathematical discoveries from program search with large language models.Nature, 625(7995)...

    2024

  27. [35]

    Learning a sat solver from single-bit supervision.arXiv preprint arXiv:1802.03685, 2018

    Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a sat solver from single-bit supervision.arXiv preprint arXiv:1802.03685, 2018

    2018 arXiv

  28. [36]

    An in-context learning agent for formal theorem-proving.arXiv preprint arXiv:2310.04353, 2023

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving.arXiv preprint arXiv:2310.04353, 2023

    2023 arXiv

  29. [37]

    The Coq proof assistant.https://coq.inria.fr/

    The Coq Development Team. The Coq proof assistant.https://coq.inria.fr/. Accessed: 2024-02-29

    2024

  30. [38]

    Lego-prover: Neural theorem proving with growing libraries.arXiv preprint arXiv:2310.00656, 2023

    Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries.arXiv preprint arXiv:2310.00656, 2023

    arXiv

  31. [39]

    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

  32. [40]

    Proving theorems recursively.arXiv preprint arXiv:2405.14414, 2024

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

    2024 arXiv

  33. [41]

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

    2025 arXiv

  34. [42]

    Kimina-prover: Kimina-prover: Applying test-time rl search on large formal reasoning models

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

    2025

  35. [43]

    Learning to prove theorems by learning to generate theorems.Advances in neural information processing systems, 33:18146–18157, 2020

    Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems.Advances in neural information processing systems, 33:18146–18157, 2020

    2020

  36. [44]

    Premise selection for theorem proving by deep graph embedding

    Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017

    2017

  37. [45]

    Holophrasm: a neural automated theorem prover for higher-order logic

    Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016

    2016 arXiv

  38. [46]

    Autoformalization with large language models.Advancesin Neural Information Processing Systems, 35: 32353–32368, 2022

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

    2022

  39. [47]

    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

  40. [48]

    Lean-github: Compiling github lean repositories for a versatile lean prover.arXiv preprint arXiv:2407.17227, 2024

    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

  41. [49]

    Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data.arXiv preprint arXiv:2405.14333, 2024

    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

  42. [50]

    Bfs- prover: Scalable best-first tree search for llm-based automatic theorem proving.arXiv preprint arXiv:2502.03438, 2025

    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

    2025

  43. [51]

    miniF2F-lean4: A collection of formal-to-formal statements and proofs in Lean 4.https://github

    Kaiyu Yang. miniF2F-lean4: A collection of formal-to-formal statements and proofs in Lean 4.https://github. com/yangky11/miniF2F-lean4, 2023

    2023

  44. [52]

    Learning to prove theorems via interacting with proof assistants

    Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. InInternational Conference on Machine Learning, pages 6984–6994. PMLR, 2019

    2019

  45. [53]

    Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023

    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:21573–21612, 2023

    2023

  46. [54]

    Leanabell-prover: Posttraining scaling in formal reasoning.arXiv preprint arXiv:2504.06122, 2025

    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

  47. [55]

    Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving.arXiv preprint arXiv:2305.16366, 2023

    Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving.arXiv preprint arXiv:2305.16366, 2023

    2023 arXiv

  48. [56]

    Subgoalxl: Subgoal- based expert learning for theorem proving.arXiv preprint arXiv:2408.11172, 2024

    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

  49. [57]

    Lyra: Orchestrating dual correction in automated theorem proving.arXiv preprint arXiv:2309.15806, 2023

    Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving.arXiv preprint arXiv:2309.15806, 2023. 17

    2023 arXiv

  50. [58]

    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

  51. [59]

    We start by considering the definition of 'even number' as applied to `n`

    Qihao Zhu, Daya Guo, Zhihong Shao, Dejian Yang, Peiyi Wang, Runxin Xu, Y Wu, Yukun Li, Huazuo Gao, Shirong Ma, et al. Deepseek-coder-v2: Breaking the barrier of closed-source models in code intelligence.arXiv preprint arXiv:2406.11931, 2024. 18 Appendix A Prompt Templates In t...

    2024 arXiv

Pith tools

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