Pith. sign in

REVIEW 3 major objections 4 minor 42 references

Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

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

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

Pith's one-line read A formal-reasoning benchmark is only complete when it ships statements and proofs in both formal and informal language, verified by its creators.

desk verdict Useful position paper on benchmark completeness for formal reasoning; the headline re-evaluation numbers lack a protocol and the feasibility estimate omits half the work—worth refereeing. read the letter →

arxiv 2507.04719 v1 pith:CPZWOG7U submitted 2025-07-07 cs.AI cs.LGcs.LO

Roozbeh Yousefzadeh , Xuenan Cao This is my paper
classification cs.AIcs.LGcs.LO
keywords completebenchmarkformalproofsinformalautoformalizationautomatedtheoremprovingLLMevaluationLeanopendata
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 argues that the field of formal reasoning—automated theorem proving and autoformalization with large language models—is being slowed by incomplete benchmarks and opaque evaluation. A benchmark, it says, is complete only when it contains four pieces: the formal statement, the informal statement, the formal proof, and the informal proof, all checked by the people who release it. The authors build the case from observed failures: errors in miniF2F took years to surface, a recent Putnam benchmark asks users to keep proofs private, and an autoformalization model reported at 97 percent accuracy measured only 67 percent when a Lean expert checked the output. If the position holds, releasing a benchmark would mean taking responsibility for the correctness and provability of every theorem in it, which would lower the barrier for newcomers and make accuracy numbers more trustworthy.

What carries the argument

The load-bearing object is the four-part complete benchmark: formal statement, informal statement, formal proof, and informal proof. It carries the argument because each part does distinct work: formal proofs certify provability, informal statements anchor autoformalization, informal proofs let humans and LLMs compare reasoning, and formal statements define the automated-theorem-proving task. The second mechanism is the human expert check on LLM judges: the paper's own reproduction of the Herald pipeline yields 97 percent while a Lean expert's manual check yields 67 percent, which is the concrete evidence that unverified automated evaluation inflates accuracy.

What would settle it

Select a recently released ATP benchmark of a few hundred problems, time a Lean-proficient researcher to write and verify the formal proofs for all of them, and see whether the total effort fits the paper's 'few months' estimate; if the true cost is several person-years, the proposed completeness norm would make benchmark creation prohibitive for small teams. Independently, take the reported 97 percent autoformalization accuracy and have two Lean experts manually check the same sample; a much smaller gap than the reported 97-to-67 would weaken the claim that LLM judges systematically inflate accuracy.

Watch

Extended reading notes

Core claim

The central claim is normative: benchmarks for formal reasoning should be complete, meaning they should contain formal problem statements, informal problem statements, formal proofs, and informal proofs, with the creators verifying all four components before release. Completeness is not decoration; it is what guarantees that every theorem in a benchmark is provable and that the informal and formal versions actually say the same thing. The paper also claims that evaluation of autoformalization cannot yet be delegated to an LLM judge, reporting that the literature's state-of-the-art accuracy of 97 percent drops to 67 percent under manual expert checking. The supporting observation is that incomplete benchmarks create parallel redundant labor and hide how far model outputs are from correct proofs, while the reported 97-versus-67 gap shows that unvalidated automated evaluation can mislead the field.

Load-bearing premise

The argument assumes a person already fluent in Lean can write and verify formal proofs for all theorems in a typical benchmark within a few months, so requiring verified proofs for every new benchmark is a reasonable cost for its creators.

Editorial extensions

If this is right

  • Future ATP benchmarks will be expected to ship all four components, making unprovable or misformalized theorems detectable at release time rather than years later.
  • Autoformalization accuracy claims will need human verification or a validated LLM judge before being published as state of the art.
  • Releasing formal proofs for existing benchmarks will reduce redundant manual proof-writing and let small research groups study failure cases without first learning Lean.
  • Evaluation reports will include proof lengths, solver-only proofs, and training-data transparency alongside raw accuracy.
  • Benchmark creators, not the community, will bear the burden of completing and correcting the data, shifting how credit is assigned in the field.

Reading between the lines

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

  • A likely consequence the paper does not spell out is a two-tier benchmark ecosystem: large well-funded groups can meet the completeness norm, while small groups may shift toward conjecturing or informal-reasoning benchmarks that do not require formal proofs.
  • The 97-to-67 gap suggests a calibration path: LLM judges could be retained but must first be validated on human-checked samples, turning the paper's warning into a concrete evaluation protocol.
  • Complete benchmarks could become living artifacts with versioned errata and proof updates, since a one-time proof check does not guard against future changes in a formal library such as Lean's Mathlib.
  • If completeness becomes standard, accuracy on a benchmark may saturate quickly, pushing the field toward harder signals such as proof length, proof quality, or difficulty-weighted pass rates rather than binary success.
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

3 major / 4 minor

Summary. This position paper argues that the formal reasoning and automated theorem proving community should adopt a norm of "complete" benchmarks, defined as containing formal and informal problem statements together with formal and informal proofs, all verified by the benchmark creators. It further advocates open release of training data, fine-tuning and evaluation code, and formal proofs; criticizes current practices such as withholding proofs and relying on LLM judges for autoformalization evaluation; and reports several concrete alleged failures, including errors in miniF2F, an incomplete BFS-Prover proof, and a claimed 97%-versus-67% discrepancy between LLM-judged and human-checked accuracy for the Herald system. The paper is explicitly a position piece rather than an empirical study, and its central recommendation is normative.

Significance. If its empirical claims withstand scrutiny, the paper identifies a real and timely problem: benchmark incompleteness and opaque evaluation practices can distort progress measures in formal reasoning. The concrete examples—miniF2F errors, the swap-ending BFS-Prover proof, DeepSeek-Prover's use of the validation set, and the Herald evaluation discrepancy—are valuable and falsifiable. The proposed four-component completeness criterion is a clear, actionable standard that could improve dataset quality and lower barriers for researchers who are not Lean experts. The paper does not ship machine-checked proofs, reproducible code, or a formal derivation; its contribution is as a critical position statement. Its main weakness is that the most striking empirical assertions are not accompanied by protocols, data, or artifacts, and the feasibility assumption underlying the central proposal is asserted rather than demonstrated.

major comments (3)
  1. [§4.2] The claim that Herald's reported 97% accuracy is actually 67% under manual checking is load-bearing for the paper's position on LLM-based evaluation, but no protocol is described: the sample size, selection criteria, definition of a correct translation, number of human annotators, inter-annotator agreement, and examples of disagreements are all absent. Without this information the reader cannot assess whether the discrepancy is real, how large it is, or whether the manual check used a stricter standard than the benchmark's own ground truth. The authors should provide the full re-evaluation protocol and ideally release the annotated judgments.
  2. [§1.1 and §3, item 3] The central proposal that all new ATP benchmarks should ship verified formal proofs, informal proofs, and matching informal statements rests on the feasibility assumption that 'a person familiar with Lean can write the formal proofs for all the problems in the dataset in a time frame of several months.' This claim is unsupported: no time logs, no release artifacts, and no independent replication are cited. The estimate also appears to omit two of the four required components: writing high-quality informal proofs and cross-checking formal-informal statement equivalence, which §3 item 3 itself says is mismatched for about half of miniF2F. The authors should supply concrete cost evidence or explicitly restrict the completeness norm to benchmarks where the creators can realistically produce all four components, otherwise the proposal may inadvertently favor large industrial teams with extensive formalization resources, recreating the barrier the paper argues against.
  3. [§5] The argument that releasing proofs does not devalue a benchmark depends on the assertion that after the release of the IMO proofs in miniF2F, 'most of those problems remain unproved by the best provers.' This is an empirical claim presented without a specification of which models were tested, under what attempt budgets, on which theorem set, and as of what date. Since the paper elsewhere criticizes evaluations that omit such details, it should hold its own counterargument to the same standard, e.g., by reporting the evaluation configuration or citing a public reproducible evaluation.
minor comments (4)
  1. [§2, item 1] The reference to 'Hu et al.' is incomplete; the bibliography lists a paper by Hu, Zhu, and Welleck (miniCTX) but the in-text citation lacks both the year and the full author list, making it hard to locate.
  2. [§4.1, item 3] There is a typo in 'The staring point for ATP models'—it should read 'starting point.'
  3. [Appendix A] In the sentence 'because the correctness and speed of any such algorithm can be easily verified automatically by a Python script,' the word 'vbe' appears as a typo for 'be.'
  4. [§4.1, item 1] The claim about DeepSeek-Prover v1.5 being trained on the miniF2F validation set and the reported 64% pass@32 accuracy would benefit from a precise pointer to the relevant passage in the cited work and a description of the authors' own evaluation setup, since this example is used to argue for transparency.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a normative position essay, not a derivation, and its central claims are supported by external examples and independent manual checks.

full rationale

This is a position paper advocating for complete benchmarks in formal reasoning, rather than a paper deriving predictions from fitted inputs. Its central proposal—that new ATP benchmarks should include formal statements, informal statements, formal proofs, and informal proofs—is a normative recommendation supported by community-practice arguments, examples such as miniF2F and Putnam Bench, and the authors' reported manual re-evaluation of Herald's 97% accuracy down to 67%. None of these steps reduces to the proposal itself by construction. The only self-citation, Yousefzadeh et al. (2025), appears in Section 5 as evidence that releasing IMO proofs did not devalue miniF2F; this is ancillary to the main advocacy and refers to a released dataset artifact, so it is not load-bearing circularity. The paper's feasibility assumption that one Lean-literate person can write formal proofs for all problems in several months is an unsupported cost estimate, but unsupported empirical claims are a correctness or robustness concern, not circularity. No fitted parameter is renamed as a prediction, no uniqueness theorem from the authors is imported to force a choice, and no known result is merely relabeled. The core arguments are self-contained against external benchmarks and community practices.

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

The paper contributes a normative proposal rather than a formal derivation. It introduces no free parameters or invented entities. It relies on domain assumptions about Lean's reliability, on a feasibility estimate for writing proofs, and on a causal claim about what would happen if proofs were released.

assumptions (4)
  • domain assumption Lean's formal verification is an authoritative ground truth for proof correctness.
    Used throughout (e.g., Section 4.2) to argue that formal proofs are reliable while LLM-based evaluations are not.
  • domain assumption The primary goal of the field is collective accelerated progress, so community norms that create barriers are to be reduced.
    Normative premise underlying the entire position; introduced in Section 1 and Conclusions.
  • ad hoc to paper Releasing ground-truth proofs will not lead to trivial saturation of benchmarks because training models to reproduce proofs is nontrivial.
    Stated in Section 5 as a counterargument to the devaluation concern; no empirical demonstration is provided in this paper.
  • ad hoc to paper A single person familiar with Lean can write formal proofs for all miniF2F theorems within a few months.
    Invoked in Sections 1.1 and 3 to argue that complete benchmarks are feasible; no evidence or log is provided.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs." pith.science (2026). https://pith.science/paper/CPZWOG7U

@misc{pith2026250704719,
  author       = {Pith},
  title        = {Pith review of: Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CPZWOG7U}},
  note         = {Machine review of arXiv:2507.04719}
}
read the original abstract

This position paper provides a critical but constructive discussion of current practices in benchmarking and evaluative practices in the field of formal reasoning and automated theorem proving. We take the position that open code, open data, and benchmarks that are complete and error-free will accelerate progress in this field. We identify practices that create barriers to contributing to this field and suggest ways to remove them. We also discuss some of the practices that might produce misleading evaluative information. We aim to create discussions that bring together people from various groups contributing to automated theorem proving, autoformalization, and informal reasoning.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

42 extracted references · 31 canonical work pages

  1. [1]

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

    work page 2025

  2. [2]

    Kasparov and Deep Blue: The historic chess match between man and machine

    Bruce Pandolfini. Kasparov and Deep Blue: The historic chess match between man and machine. Simon and Schuster, 1997

    work page 1997

  3. [3]

    Mastering the game of Go without human knowledge

    David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of Go without human knowledge. Nature, 550 0 (7676): 0 354--359, 2017

    work page 2017

  4. [4]

    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 25th International Conference on Automated Deduction, pages 378--388, 2015

    work page 2015

  5. [5]

    Mathematical reasoning and the computer

    Kevin Buzzard. Mathematical reasoning and the computer. Bulletin of the American Mathematical Society, 2024

    work page 2024

  6. [6]

    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 . In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23, 2023. URL https://openreview.net/forum?id=C9X5sXa2k1

    work page 2023

  7. [7]

    Formalizing a proof in Lean using Claude and o4, 2025

    Terence Tao. Formalizing a proof in Lean using Claude and o4, 2025. URL https://youtu.be/zZr54G7ec7A

    work page 2025

  8. [8]

    Intelligent machinery, a heretical theory

    Alan M Turing. Intelligent machinery, a heretical theory. Philosophia Mathematica, 4 0 (3), 1948

    work page 1948

Show all 42 references
  1. [9]

    Generative language modeling for automated theorem proving, 2020

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020. URL https://arxiv.org/abs/2009.03393

    2020 arXiv

  2. [10]

    Learning to prove theorems via interacting with proof assistants

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

    2019

  3. [11]

    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 International Conference on Learning Representations, 2021

    2021

  4. [12]

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

    2022

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

    2022

  6. [14]

    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. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=Se6MgCtRhz

    2025

  7. [15]

    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

  8. [16]

    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. In The Thirty-eight Conference on Neural Information Processi...

    2024

  9. [17]

    AI achieves silver-medal standard solving international mathematical olympiad problems

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

    2024

  10. [18]

    BFS-Prover : Scalable best-first tree search for llm-based automatic theorem proving, 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, 2025. URL https://arxiv.org/abs/2502.03438

    2025

  11. [19]

    LeanDojo : Theorem proving with retrieval-augmented language models

    Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo : Theorem proving with retrieval-augmented language models. In Thirty-seventh Conference on Neural Information Processing Systems Datasets an...

    2023

  12. [20]

    miniCTX : Neural theorem proving with (long-) contexts

    Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX : Neural theorem proving with (long-) contexts. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24

  13. [21]

    Formalmath: Benchmarking formal mathematical reasoning of large language models

    Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, et al. Formalmath: Benchmarking formal mathematical reasoning of large language models. arXiv preprint arXiv:2505.02735, 2025

    2025 arXiv

  14. [22]

    Isabelle: A generic theorem prover

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

    1994

  15. [23]

    The Coq proof assistant: a tutorial

    G \'e rard Huet, Gilles Kahn, and Christine Paulin-Mohring. The Coq proof assistant: a tutorial. Rapport Technique, 178: 0 113, 1997

    1997

  16. [24]

    ImageNet : A large-scale hierarchical image database

    Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. ImageNet : A large-scale hierarchical image database. In IEEE Conference on Computer Vision and Pattern recognition, pages 248--255, 2009

    2009

  17. [25]

    Autoformalizing Euclidean geometry

    Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing Euclidean geometry. In Forty-first International Conference on Machine Learning, 2024

    2024

  18. [26]

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

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover: A frontier model for open-source automated theorem proving, 2025. URL https://arxiv.org/abs/2502.07640

    2025 arXiv

  19. [27]

    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 a

    2024 arXiv

  20. [28]

    Formal conjectures

    Google DeepMind. Formal conjectures. https://github.com/google-deepmind/formal-conjectures, 2024. GitHub repository

    2024

  21. [29]

    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, Zhenguo Li, and Xiaodan Liang. LEGO-Prover : Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Repres...

    2024

  22. [30]

    Large language model benchmarks do not test reliability

    Joshua Vendrow, Edward Vendrow, Sara Beery, and Aleksander Madry. Large language model benchmarks do not test reliability. In NeurIPS Safe Generative AI Workshop 2024, 2024. URL https://openreview.net/forum?id=XSeN6xZtZ9

    2024

  23. [31]

    Do ImageNet classifiers generalize to ImageNet ? In International Conference on Machine Learning, pages 5389--5400, 2019

    Benjamin Recht, Rebecca Roelofs, Ludwig Schmidt, and Vaishaal Shankar. Do ImageNet classifiers generalize to ImageNet ? In International Conference on Machine Learning, pages 5389--5400, 2019

    2019

  24. [32]

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

    2024 arXiv

  25. [33]

    Mathesis: Towards formal theorem proving from natural languages

    Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, et al. Mathesis: Towards formal theorem proving from natural languages. arXiv preprint arXiv:2506.07047, 2025

    2025 arXiv

  26. [34]

    Autoformalize mathematical statements by symbolic equivalence and semantic consistency

    Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openrev...

    2024

  27. [35]

    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. Transactions on Machine Learning Research, 2025. ISSN 2835-8856. URL https://openreview.net/forum?id=CrKMqRAhBo

    2025

  28. [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, 2022

    2022

  29. [37]

    Scientific discovery in the age of artificial intelligence

    Hanchen Wang, Tianfan Fu, Yuanqi Du, Wenhao Gao, Kexin Huang, Ziming Liu, Payal Chandak, Shengchao Liu, Peter Van Katwyk, Andreea Deac, et al. Scientific discovery in the age of artificial intelligence. Nature, 620 0 (7972): 0 47--60, 2023

    2023

  30. [38]

    Mathematical discoveries from program search with large language models

    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, pages 1--3, 2023

    2023

  31. [39]

    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, 625 0 (7995): 0 476--482, 2024

    2024

  32. [40]

    Competition-level code generation with AlphaCode

    Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, R \'e mi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, et al. Competition-level code generation with AlphaCode . Science, 378 0 (6624): 0 1092--1097, 2022

    2022

  33. [41]

    AlphaEvolve : A learning framework to discover novel alphas in quantitative investment

    Can Cui, Wei Wang, Meihui Zhang, Gang Chen, Zhaojing Luo, and Beng Chin Ooi. AlphaEvolve : A learning framework to discover novel alphas in quantitative investment. In Proceedings of the 2021 International conference on management of data, pages 2208--2216, 2021

    2021

  34. [42]

    Welcome to the era of experience

    David Silver and Richard S Sutton. Welcome to the era of experience. Google AI, 2025

    2025

Pith tools

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