Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

Formally Solving Answer-Construction Problems in Lean

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

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

Pith's one-line read The paper claims ECP, a pipeline that enumerates candidate answers in Python, conjectures them in Lean, and proves them with a prover LLM, raises formal PutnamBench answer-construction solves from 4 to 6 and end-to-end ConstructiveBench…

desk verdict A genuinely new benchmark and a workable enumerate-conjecture-prove recipe, but the 'formally solves' claim is undermined by the benchmark's own 17% major-error audit and an abstract that doesn't match the body. read the letter →

arxiv 2505.18492 v6 pith:NZ3PTLDJ submitted 2025-05-24 cs.AI

Jialiang Sun , Yuzhi Tang , Ao Li , Chris J. Maddison , Kuldeep S. Meel This is my paper
classification cs.AI
keywords answerconstructionLeantheoremprovingautoformalizationneuro-symbolicreasoningLLMenumerationConstructiveBenchPutnammathematicalcompetitionproblems
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 targets answer-construction problems, 'find all objects satisfying these conditions,' which it argues are under-served compared with theorem-proving problems. It proposes the Enumerate, Conjecture, Prove (ECP) framework, in which a general LLM writes Python programs to enumerate small candidate answers, a conjecturing LLM uses those enumerations as hints to propose a closed-form Lean answer, and a prover LLM produces a machine-checked proof in Lean. On the paper's measurements, ECP consistently beats a chain-of-thought baseline across six conjecturers and three provers, lifting end-to-end accuracy on the new ConstructiveBench dataset from 32.5% to 33.1% and raising formal solves on the PutnamBench answer-construction subset from 4 to 6 of 337 problems. A sympathetic reader would care because this is one of the first systematic templates for getting formal, verifiable answers to 'find all X' competition problems rather than informal answer-only outputs.

What carries the argument

The Enumerate, Conjecture, Prove (ECP) loop is the mechanism: an LLM writes Python programs, bounded to 100 enumerated answers within a 60-second timeout, to probe small or parameterized cases; a conjecturing LLM is prompted with the task and the enumeration as hints to produce a syntactically valid Lean answer expression, with a system-prompt prohibition against answers that echo the problem statement or render it vacuous; and a prover LLM (DeepSeek-Prover-V2-7B, Goedel-Prover-SFT, or Kimina-Prover-Preview-7B) attempts to close the Lean goal after substitution. The formal backbone is the task statement $\exists f : \alpha \to \mathrm{Set}\,\beta,\ \forall a : \alpha,\ P(a) \to \forall b : \beta,\ Q(a,b) \leftrightarrow b \in f(a)$, whose function $f$ is the admissible closed-form answer set that ECP must produce.

What would settle it

Take the six PutnamBench problems ECP claims to solve end-to-end, have human experts check the Lean formalizations against the original Putnam statements, and attempt to construct the same solution from the informal problem alone; if any formalization is materially unfaithful to the original problem, that formal solve does not constitute a solution to the stated competition problem, and the headline claim weakens proportionally.

Watch

Extended reading notes

Core claim

The central claim is that answer-construction in a proof assistant is best solved by splitting the work across LLM specialities: a general LLM enumerates candidate answers by generating and running Python programs, then reasons from the enumeration to conjecture a canonical closed-form answer in Lean, and a separate prover LLM proves the substituted theorem in Lean, with the Lean compiler serving as the verifier. The paper formalizes the task as the construction of an answer function $f: \alpha \to \mathrm{Set}\,\beta$ such that for every context $a$ satisfying the context property $P$, $Q(a,b) \leftrightarrow b \in f(a)$, and it reports that this pipeline consistently improves answer construction and formally solves 6 out of 337 answer-construction problems end-to-end on PutnamBench (up from 4 without ECP) using GPT-5 mini and DeepSeek-Prover-V2-7B, plus 33.1% end-to-end accuracy on the 3,640-problem ConstructiveBench dataset. The paper interprets these gains as evidence that combining LLM-driven enumeration and conjecturing with formal verification is a productive direction for competition-level answer-construction problems.

Load-bearing premise

The load-bearing premise is that the autoformalized Lean statements say what the original competition problems say; the paper's own human evaluation of 100 sampled statements found 17 major errors, so the solve counts inherit real uncertainty.

Editorial extensions

If this is right

  • If ECP is right, answer-construction problems in Lean decompose into independent sub-problems, enumeration, conjecture, and proof, so any improvement in a component transfers directly to end-to-end solve rates.
  • Every conjecturer model the paper tests improves with ECP, and the largest gains are for lightweight non-reasoning models (DeepSeek-V3 jumps from 17.3% to 40.7% on ConstructiveBench answer construction), suggesting enumeration signals can partially compensate for weaker reasoning models.
  • CoT and ECP solve overlapping but distinct problem subsets, since union accuracy consistently exceeds either method, so a practical system would run both and take the union.
  • The 106-problem after-cutoff split reproduces the improvement pattern, so the reported gains are not purely an artifact of memorized training problems.
  • The autoformalized ConstructiveBench dataset gives the community a shared, Lean-checkable ground for measuring 'find all' problems, not just theorem proving.

Reading between the lines

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

  • Editorial inference: because the paper's own human audit found 17 major errors in 100 sampled formalizations, the honest measure of the method is probably on a human-verified subset; auditing the 6 Putnam solves against the original statements would be the decisive check.
  • Editorial inference: admissibility is enforced only by a system prompt, so solving a problem formally still allows a model to cheat semantically by echoing the statement; this could be closed by formalizing a non-circularity condition as a checkable Lean predicate.
  • Editorial inference: the approach could transfer beyond competitions to 'find all' problems in research math, but its bounded enumeration (max 100 candidates) limits it to problems whose answer spaces are small or pattern-generable in Python.
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 / 4 minor

Summary. The paper introduces ECP (Enumerate-Conjecture-Prove), a neuro-symbolic framework for answer-construction problems in Lean, and ConstructiveBench, a dataset of 3,640 autoformalized competition problems. ECP uses a general LLM to enumerate candidate answers via Python, a conjecturer LLM to propose a closed-form Lean answer, and a prover LLM to close the resulting theorem statement. The body reports consistent improvements over a chain-of-thought baseline, including end-to-end accuracy of 33.1% versus 32.5% on ConstructiveBench and 6 versus 4 solved PutnamBench problems with GPT-5 mini and DeepSeek-Prover-V2-7B. The abstract, however, claims 17/346 PutnamBench and 18/75 MathArena instances, numbers that do not match the body and do not correspond to any experiment described in the paper.

Significance. If the reported results were established, the paper would make a useful contribution: it proposes a modular, model-agnostic pipeline that combines code-based enumeration with formal proving, and it ships public code and data, including machine-checked proofs and a human audit of formalization quality. The after-cutoff split is a valuable contamination control. However, the central quantitative claims depend on the fidelity of the autoformalized ground-truth statements, and the paper's own audit indicates a 17% major-error rate in those statements, so the significance is conditional and, on current evidence, not established.

major comments (4)
  1. [Abstract; §5.3; Table 3] The abstract's headline numbers are inconsistent with the body. The abstract states that ECP formally solves 17/346 PutnamBench instances and 18/75 MathArena instances, whereas Section 5.3 reports 6 out of 337 PutnamBench problems end-to-end and Table 3 shows 4 versus 6 for the GPT-5 mini configuration; no MathArena experiment appears anywhere in the body. The denominator discrepancy (346 versus 337) and the appearance of an unmentioned dataset mean the central claim as advertised in the abstract is not supported by the described experiments. This must be resolved before the paper can be evaluated fairly.
  2. [§4.4; Appendix C; §5.1] The ground-truth fidelity of ConstructiveBench is load-bearing and is undermined by the authors' own human audit. Section 4.4 reports that 17 of 100 randomly sampled accepted formalizations have major errors, and Appendix C gives a concrete example (IMO2023SLN7) in which the formal statement has a different logical shape from the original problem. Since answer-construction accuracy is defined in Section 5.1 as provable equality to the ground-truth answer, and end-to-end success is measured against those same statements in Tables 2 and 3, all reported accuracies may count solutions to statements that do not represent the original competition problems. The acceptance criteria in Section 4.3 (Lean compiles plus an LLM judge) are not sufficient evidence of semantic fidelity, as the audit itself demonstrates.
  3. [§3.2; Abstract] The abstract claims that ECP 'introduces admissibility checking to ensure that each answer is canonical and does not involve a circular argument,' but Section 3.2 implements this only as a system-prompt instruction that disallows illegal answers. There is no formal or machine-checked admissibility condition in the pipeline, and the evaluation does not verify that conjectured answers are admissible. The 'admissible answers and proofs' phrasing in the abstract is therefore not supported by the mechanism described in the paper; if admissibility is essential to the method, it should be a formal condition rather than a prompt.
  4. [§5.3; Tables 2–3] The headline end-to-end gains are extremely small and are reported without any statistical support. On ConstructiveBench the improvement is 33.1% versus 32.5% (roughly 22 problems out of 3,640), and on PutnamBench it is 6 versus 4 problems out of 337. No confidence intervals, significance tests, or error bars are reported. Given the measured 17% major-error rate in the ground truth, these differences are within the noise of the benchmark's own labeling errors, and the claim that ECP 'consistently improves' answer construction is not established on the evidence presented.
minor comments (4)
  1. [References] The reference list appears twice in full (pages 10–16); the duplicate should be removed.
  2. [Appendix B.3] The conjecturing prompt contains a typo: 'exprssion' should be 'expression'.
  3. [Table 3] The table formatting for the end-to-end columns, e.g. '4 /66' and '4 / 4 5', is confusing and should use clear column separators so the CoT, ECP, and Union values are unambiguous.
  4. [§5.2; Table 7] The main text states that after-cutoff results show robustness when contamination is controlled, but Table 7 notes that DeepSeek-V3.1 has a knowledge cutoff after June 2024 and its after-cutoff accuracy may be contaminated; this caveat should be reflected in the main text.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: ECP's headline numbers are measured against externally fixed Lean ground-truth statements; the paper's acknowledged autoformalization errors are a correctness risk, not a circular derivation chain.

full rationale

The central claim is empirical: ECP improves answer-construction and end-to-end accuracy over a CoT baseline. The evaluation compares ECP's conjectured answers to ground-truth Lean expressions using Lean automation tactics, and end-to-end solving additionally requires a Lean-checked proof after substituting the conjectured answer. The ground-truth expressions are fixed before ECP runs; ECP never receives them in the enumeration or conjecture prompts. No parameter is fitted to the test set, and no reported number is a function of ECP's own output. The paper's self-citations (e.g., APPL for prompt programming, the theorem-proving survey, PyEuclid in related work) are implementation or related-work references, not load-bearing evidence for ECP's efficacy. The autoformalization-quality limitation acknowledged in Section 6, together with the 17/100 major-error human audit in Section 4.4 and Appendix C, is a threat to benchmark validity: solving a malformed Lean statement is not solving the original competition problem. But that is a correctness-risk concern, not a circular derivation, because the evaluation outcome is still an external, falsifiable fact about the fixed Lean statements. The overlap between the LLM used as autoformalization judge and as conjecturer is likewise a methodological contamination concern, not a step where a prediction is defined in terms of the fitted input. No quoted equation or procedure in the paper exhibits the pattern of a result reducing to its own inputs by construction. The appropriate finding is therefore no significant circularity.

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

No mathematical constants are fitted by a derivation; the listed values are hand-chosen evaluation budgets and thresholds. The load-bearing axioms are the reliability of the autoformalized statements and the LLM judge, both of which the paper's own human audit partially refutes: 17% major errors in a sample of 100.

free parameters (8)
  • max_enumerated_answers = 100
    System prompt caps enumeration at 100 answers (Section 3.2); results for infinite-answer problems depend on this cap.
  • enumerate_stage_timeout = 60s
    Per-call timeout in the Enumerate stage (Section 3.2); larger budgets may change enumeration coverage.
  • coder_max_attempt = 3
    Maximum refinement attempts for the enumerator (Section 5.1).
  • conjecturing_attempt = 5
    Maximum refinement attempts for the conjecturer (Section 5.1).
  • autoformalization_iterations = 5
    T = 5 refinement iterations per model in the autoformalization loop (Section 4.3).
  • pass_at_k = 32
    Pass@32 sampling budget for the prover (Section 5.1); higher k would raise reported accuracy.
  • lean_verification_timeout = 120s
    Lean verification timeout in evaluation (Section 5.1).
  • dedup_similarity_threshold = 0.9
    90% semantic-similarity threshold for deduplication (Section 4.2).
assumptions (5)
  • standard math Lean 4 and mathlib are sound
    The verifier is trusted; no axioms of Lean are stated.
  • domain assumption LLM-judge semantic equivalence is reliable
    Section 4.3 accepts a formalization only if the Lean compiles and the GPT-5 mini judge deems it semantically equivalent; this is not a formal check and is shown by the authors' human eval to fail for 17% of a 100-sample (Appendix C).
  • domain assumption Ground-truth answers in source competitions are correct and unique
    ConstructiveBench inherits answers from OlympiadBench, Omni-Math, MathOdyssey and official archives (Section 4.1); errors in sources would propagate.
  • domain assumption Autoformalized Lean statements match the original informal problems
    The whole evaluation treats a solved Lean statement as a solved competition problem; the human evaluation in Section 4.4 indicates this assumption fails for 17% of sampled problems.
  • domain assumption The tactic set (simp, aesop, nlinarith, ring, norm_num) decides answer equality
    Answer-construction accuracy is defined by provable equality to ground truth using these tactics (Section 5.1); failures could be due to tactic incompleteness rather than wrong answers.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formally Solving Answer-Construction Problems in Lean." pith.science (2026). https://pith.science/paper/NZ3PTLDJ

@misc{pith2026250518492,
  author       = {Pith},
  title        = {Pith review of: Formally Solving Answer-Construction Problems in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NZ3PTLDJ}},
  note         = {Machine review of arXiv:2505.18492}
}
read the original abstract

Large language models (LLMs) have achieved remarkable progress in formal mathematical reasoning. Mathematical competition problems fall into two broad types: theorem-proving problems ask for a proof of a fully specified statement, whereas answer-construction problems ask the solver to construct an answer object and prove that it satisfies the stated specification. Existing mathematical reasoning engines mainly target theorem-proving problems, yet answer-construction problems remain less studied. This setting is challenging because model capabilities are misaligned, with general LLMs better suited to answer construction and prover LLMs better suited to proof generation, and because Lean proof checking alone does not rule out inadmissible circular witnesses. To close this gap, we introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework for solving answer-construction problems in Lean. ECP uses general LLMs to perform bounded enumeration and construct candidate answers, and invokes prover LLMs to produce machine-checked proofs. ECP introduces admissibility checking to ensure that each answer is canonical and does not involve a circular argument. On answer-construction problems from PutnamBench and autoformalized MathArena, ECP formally solves 17/346 PutnamBench instances and 18/75 MathArena instances with admissible answers and proofs, outperforming LLM baselines at aligned inference budgets.

Figures

Figures reproduced from arXiv: 2505.18492 by the authors.

Figure 1
Figure 1. Illustration of the ECP framework applied to a formalized Balkan MO Shortlist problem in [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Problem sources and domains in ConstructiveBench. Only the top 11 sources and top 7 [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Overview of the autoformalization pipeline: the LLM drafts a formal statement; when [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: shows an example dataset entry and the distribution of answer types. The diversity of answer types enables comprehensive evaluation across a wide range of problem formats [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]

Discussion (0). Sign in 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. Discovering Ordinary Differential Equations with LLM-Based Qualitative and Quantitative Evaluation

    cs.AI 2026-05 unverdicted novelty 6.0 of 10

    DoLQ employs a sampler agent, parameter optimizer, and LLM-based scientist agent to iteratively propose, refine, and evaluate ODE candidates, yielding higher success rates and better symbolic term recovery than prior ...

Reference graph

Works this paper leans on

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

  1. [1]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should not add it explicitly Type <Return> for now, but then later remove the command n...

  2. [2]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@first@sw \@firstoftwo \@ifundefined NAT@b*@#2 \@firstoftwo @num @NAT@ctr \@secondoft...

  3. [3]

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibsetup #1 @NAT@ctr @ @openbib .11em \@plus.33em \@minus.07em 4000 4000 `\.\@m @bibit...

    work page

  4. [4]

    Mathqa: Towards interpretable math word problem solving with operation-based formalisms

    Aida Amini, Saadia Gabriel, Peter Lin, Rik Koncel-Kedziorski, Yejin Choi, and Hannaneh Hajishirzi. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 2357--2367, 2019

    work page 2019

  5. [5]

    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

    arXiv 2023

  6. [6]

    Mathconstruct: Challenging llm reasoning with constructive proofs

    Mislav Balunovi \'c , Jasper Dekoninck, Nikola Jovanovi \'c , Ivo Petrov, and Martin Vechev. Mathconstruct: Challenging llm reasoning with constructive proofs. arXiv preprint arXiv:2502.10197, 2025

    arXiv 2025

  7. [7]

    Matharena: Evaluating llms on uncontaminated math competitions, February 2025

    Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. Matharena: Evaluating llms on uncontaminated math competitions, February 2025. URL https://matharena.ai/

    2025

  8. [8]

    CVC5: A Versatile and Industrial-Strength SMT Solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N \"o tzli, et al. CVC5: A Versatile and Industrial-Strength SMT Solver . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2022

    work page 2022

Show all 59 references
  1. [9]

    Sledgehammer: Judgement Day

    Sascha B \"o hme and Tobias Nipkow. Sledgehammer: Judgement Day . In Proceedings of the International Joint Conference on Automated Reasoning , 2010

    2010

  2. [10]

    Seed-prover: Deep and broad reasoning for automated theorem proving

    Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025

    2025 arXiv

  3. [11]

    Gold-medalist performance in solving olympiad geometry with alphageometry2

    Yuri Chervonyi, Trieu H Trinh, Miroslav Ol s \'a k, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V Le, and Thang Luong. Gold-medalist performance in solving olympiad geometry with alphageometry2. arXiv preprint arXiv:2502.03544, 2025

    2025

  4. [12]

    Training verifiers to solve math word problems

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Jacob Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021

    arXiv

  5. [13]

    Z3: An efficient SMT solver

    Leonardo De Moura and Nikolaj Bj rner. Z3: An efficient SMT solver . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008

    2008

  6. [14]

    Appl: A prompt programming language for harmonious integration of programs and large language model prompts

    Honghua Dong, Qidong Su, Yubo Gao, Zhaoyu Li, Yangjun Ruan, Gennady Pekhimenko, Chris J Maddison, and Xujie Si. Appl: A prompt programming language for harmonious integration of programs and large language model prompts. arXiv preprint arXiv:2406.13161, 2024

    2024 arXiv

  7. [15]

    The faiss library

    Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Pierre-Emmanuel Mazar \'e , Maria Lomeli, Lucas Hosseini, and Herv \'e J \'e gou. The faiss library. arXiv preprint arXiv:2401.08281, 2024

    2024 arXiv

  8. [16]

    Mathodyssey: Benchmarking mathematical problem-solving skills in large language models using odyssey math data

    Meng Fang, Xiangpeng Wan, Fei Lu, Fei Xing, and Kai Zou. Mathodyssey: Benchmarking mathematical problem-solving skills in large language models using odyssey math data. arXiv preprint arXiv:2406.18321, 2024

    2024 arXiv

  9. [17]

    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

  10. [18]

    Omni-math: A universal olympiad level mathematic benchmark for large language models

    Bofei Gao, Feifan Song, Zhe Yang, Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, et al. Omni-math: A universal olympiad level mathematic benchmark for large language models. arXiv preprint arXiv:2410.07985, 2024 a

    arXiv

  11. [19]

    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 b

    2024 arXiv

  12. [20]

    Pal: Program-aided language models

    Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. Pal: Program-aided language models. In International Conference on Machine Learning, pages 10764--10799. PMLR, 2023

    2023

  13. [21]

    Tora: A tool-integrated reasoning agent for mathematical problem solving

    Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Minlie Huang, Nan Duan, and Weizhu Chen. Tora: A tool-integrated reasoning agent for mathematical problem solving. arXiv preprint arXiv:2309.17452, 2023

    2023 arXiv

  14. [22]

    Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems

    Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, et al. Olympiadbench: A challenging benchmark for promoting agi with olympiad-level bilingual multimodal scientific problems. arXiv preprint arXiv:2402....

    2024 arXiv

  15. [23]

    Measuring mathematical problem solving with the math dataset

    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. arXiv preprint arXiv:2103.03874, 2021

    2021 arXiv

  16. [24]

    A survey on hallucination in large language models: Principles, taxonomy, challenges, and open questions

    Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, et al. A survey on hallucination in large language models: Principles, taxonomy, challenges, and open questions. ACM Transactions on Informatio...

    2025

  17. [25]

    Gemini 2.5 pro capable of winning gold at imo 2025

    Yichen Huang and Lin F Yang. Gemini 2.5 pro capable of winning gold at imo 2025. arXiv preprint arXiv:2507.15855, 2025

    2025

  18. [26]

    First-Order Theorem Proving and Vampire

    Laura Kov \'a cs and Andrei Voronkov. First-Order Theorem Proving and Vampire . In Proceedings of the International Conference on Computer Aided Verification , 2013

    2013

  19. [27]

    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 Xiaoxing Ma. Proving olympiad inequalities by synergizing llms and symbolic reasoning. In Proceedings of the International Conference on Learning Representations , 2025 a

    2025

  20. [28]

    A survey on deep learning for theorem proving, 2024

    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, 2024. URL https://arxiv.org/abs/2404.09939

    2024 arXiv

  21. [29]

    Pyeuclid: A versatile formal plane geometry system in python

    Zhaoyu Li, Hangrui Bi, Jialiang Sun, Zenan Li, Kaiyu Yang, and Xujie Si. Pyeuclid: A versatile formal plane geometry system in python. In International Conference on Computer Aided Verification, pages 405--420. Springer, 2025 b

    2025

  22. [30]

    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

  23. [31]

    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

    2025 arXiv

  24. [32]

    FIMO: A Challenge Formal Dataset for Automated Theorem Proving

    Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. FIMO: A Challenge Formal Dataset for Automated Theorem Proving . arXiv preprint arXiv:2309.04295, 2023

    2023 arXiv

  25. [33]

    Combibench: Benchmarking llm capability for combinatorial mathematics, 2025 a

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

    2025 arXiv

  26. [34]

    Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving

    Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao, and Junchi Yan. Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving. arXiv preprint arXiv:2505.04528, 2025 b

    2025 arXiv

  27. [35]

    The Lean Mathematical Library

    The mathlib Community. The Lean Mathematical Library . In Proceedings of the ACM SIGPLAN International Conference on Certified Programs and Proofs , 2020

    2020

  28. [36]

    The Lean 4 Theorem Prover and Programming Language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language . In Proceedings of the International Conference on Automated Deduction , 2021

    2021

  29. [37]

    The logic theory machine--a complex information processing system

    Allen Newell and Herbert Simon. The logic theory machine--a complex information processing system. IRE Transactions on information theory, 2 0 (3): 0 61--79, 1956

    1956

  30. [38]

    Isabelle: A Generic Theorem Prover

    Lawrence C Paulson. Isabelle: A Generic Theorem Prover . Springer , 1994

    1994

  31. [39]

    How to solve it: A new aspect of mathematical method

    George Polya. How to solve it: A new aspect of mathematical method. In How to solve it. Princeton university press, 2014

    2014

  32. [40]

    Sentence-bert: Sentence embeddings using siamese bert-networks

    Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embeddings using siamese bert-networks. arXiv preprint arXiv:1908.10084, 2019

    1908 arXiv

  33. [41]

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

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

    2025 arXiv

  34. [42]

    E--A Brainiac Theorem Prover

    Stephan Schulz. E--A Brainiac Theorem Prover . AI Communications, 2002

    2002

  35. [43]

    DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models . arXiv preprint arXiv:2402.03300, 2024

    2024 arXiv

  36. [44]

    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

  37. [45]

    Ai achieves silver-medal standard solving international mathematical olympiad problems

    AlphaProof Teams. Ai achieves silver-medal standard solving international mathematical olympiad problems. IRE Transactions on information theory, 2024

    2024

  38. [46]

    Solving Olympiad Geometry without Human Demonstrations

    Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving Olympiad Geometry without Human Demonstrations . Nature, 2024

    2024

  39. [47]

    PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical 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 Mathematical Competition . arXiv preprint arXiv:2407.11214, 2024

    2024 arXiv

  40. [48]

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

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

    2025 arXiv

  41. [49]

    Chain-of-thought prompting elicits reasoning in large language models, 2023

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models, 2023. URL https://arxiv.org/abs/2201.11903

    2023 arXiv

  42. [50]

    Autoformalization with Large Language Models

    Yuhuai Wu, Albert Q Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with Large Language Models . In Proceedings of the International Conference on Neural Information Processing Systems , 2022

    2022

  43. [51]

    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

  44. [52]

    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

  45. [53]

    React: Synergizing reasoning and acting in language models

    Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. React: Synergizing reasoning and acting in language models. In International Conference on Learning Representations (ICLR), 2023

    2023

  46. [54]

    SATLM: Satisfiability-Aided Language Models using Declarative Prompting

    Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SATLM: Satisfiability-Aided Language Models using Declarative Prompting . In Proceedings of the International Conference on Neural Information Processing Systems , 2023

    2023

  47. [55]

    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 a

    2024 arXiv

  48. [56]

    InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning

    Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning . arXiv preprint arXiv:2402.06332, 2024 b

    2024 arXiv

  49. [57]

    Dapo: An open-source llm reinforcement learning system at scale

    Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Weinan Dai, Tiantian Fan, Gaohong Liu, Lingjun Liu, et al. Dapo: An open-source llm reinforcement learning system at scale. arXiv preprint arXiv:2503.14476, 2025 a

    2025 arXiv

  50. [58]

    Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025 b

    Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. Formalmath: Benchmarking formal mathematical reasoning of large language models, 2025 b . URL https://arxiv...

    2025 arXiv

  51. [59]

    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 . In Proceedings of the International Conference on Learning Representations , 2022

    2022

Pith tools

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