---
title: "ProofNet: Autoformalizing and Formally — Azerbayev 2023"
description: "Autoformalization means converting informal mathematics into statements a proof assistant can check."
authors: ["Zhangir Azerbayev", "Bartosz Piotrowski", "Hailey Schoelkopf", "Edward W. Ayers", "Dragomir Radev", "Jeremy Avigad"]
year: 2023
venue: "arXiv:2302.12433"
source: "https://arxiv.org/abs/2302.12433"
doi: "10.48550/arxiv.2302.12433"
arxiv: "2302.12433"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2023](https://md.research.elamur.ai/free/en/papers/2023/page/6/) / ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

# ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

**Authors:** [Zhangir Azerbayev](https://md.research.elamur.ai/free/en/authors/zhangir-azerbayev/), Bartosz Piotrowski, [Hailey Schoelkopf](https://md.research.elamur.ai/free/en/authors/hailey-schoelkopf/), Edward W. Ayers, [Dragomir Radev](https://md.research.elamur.ai/free/en/authors/dragomir-radev/), Jeremy Avigad · **Year:** 2023 · **Venue:** arXiv:2302.12433 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2302.12433) · [PDF](https://arxiv.org/pdf/2302.12433v1) · [DOI 10.48550/arxiv.2302.12433](https://doi.org/10.48550/arxiv.2302.12433) · [arXiv 2302.12433](https://arxiv.org/abs/2302.12433) · [OpenAlex](https://openalex.org/W4322616316)

**Citations:** 14 citations (openalex-snapshot · 2026-10-14) · [127](#cited-by) in our library, of the 140673 papers whose bibliographies we read

## Summary
Autoformalization means converting informal mathematics into statements a proof assistant can check. Progress has been limited by the scarcity of paired informal and formal data. Existing prover benchmarks also lean on competition problems that require only a small set of elementary facts. To address this, the authors build ProofNet: 371 exercises, mostly taken from widely used undergraduate pure-math textbooks covering analysis, algebra, number theory and topology. Each exercise comes with a Lean 3 statement built on mathlib, a LaTeX statement and an informal proof. Annotators chose problems that are self-contained and naturally formalizable. They also favoured applying general results to specific cases rather than mathlib-style general theory, which reduces overlap with pretraining data. For stronger open baselines, the team releases PROOF GPT (1.3B and 6.7B parameters). These are Pythia checkpoints further trained on the 8-billion-token proof-pile. Few-shot in-context learning with Code-davinci-002 and PROOF GPT reaches non-trivial but inconsistent statement autoformalization. Two new techniques, prompt retrieval and distilled backtranslation, improve on these baselines. The benchmark matters because it tests reasoning across a large library of definitions and theorems.

## Key points
- **ProofNet dataset:** 371 triples (Lean 3 formal statement, natural language statement, natural language proof). It is published on Hugging Face as `hoskinson-center/proofnet`, with experiment code on GitHub. It supports four tasks:
  - formal proving
  - informal proving
  - statement autoformalization/informalization
  - proof autoformalization
- **proof-pile corpus:** about 8B tokens in total. It is dominated by arXiv.math (13.6 GB, 4.9B tokens), followed by Stack Exchanges (0.3B) and formal math libraries (59M). It also includes ProofWiki + Wikipedia, open-source books and MATH.
- **PROOF GPT perplexity:** the models score lower than comparable Pythia models. On arXiv.math, the 1.3B model reaches 3.17 versus 3.82, and the 6.7B model reaches 3.12 versus 3.36. Training used the GPT-NeoX library.
- **New autoformalization methods:**
  - Prompt retrieval builds prompts from nearest-neighbour mathlib declarations found via embedding search.
  - Distilled backtranslation, inspired by unsupervised MT, fine-tunes a model without parallel data.
- **Error analysis:**
  - Models often use nonexistent mathlib names, such as `simple_group` instead of `is_simple_group`; retrieval can fix this.
  - Models omit implicit hypotheses, for example an `inner_product_space` structure.
  - Small PROOF GPT models tend to loop on repeated text, which Code-davinci-002 does not do.
  - Formal proving experiments are left to future work.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

Fields: [Mathematics & statistics](https://md.research.elamur.ai/free/en/shelves/mathematics/)

## Cited by

Cited by

127 papers of our library cite it (of the 140673 whose bibliographies we read); 8 of them have a page here, 119 not yet.

- [Llemma: An Open Language Model For Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://md.research.elamur.ai/free/en/papers/gao-2024-omni-math-universal-olympiad-level/)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://md.research.elamur.ai/free/en/papers/olausson-2023-linc-neurosymbolic-approach-logical-reasoning/)
- [OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text](https://md.research.elamur.ai/free/en/papers/paster-2023-openwebmath-open-dataset-high-quality/)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/)
- [A Survey of Large Language Models](https://md.research.elamur.ai/free/en/papers/zhao-2023-survey-large-language-models/)

## Cite

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{azerbayev2023proofnet,
  title = {{ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics}},
  author = {Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy},
  year = {2023},
  doi = {10.48550/arxiv.2302.12433},
  eprint = {2302.12433},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2302.12433}
}
```

- [← previous PromptRobust: Towards Evaluating the Robustness of Large Language Models on Adversarial Prompts](https://md.research.elamur.ai/free/en/papers/zhu-2023-promptrobust-towards-evaluating-robustness-large/)
- [next → QA-KGNet: 一种语言模型驱动的知识图谱问答模型](https://md.research.elamur.ai/free/en/papers/qiao-2023-qa-kgnet-language/)
- [↑ back to papers of 2023](https://md.research.elamur.ai/free/en/papers/2023/page/6/)

## References

40 references, 13 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Alex Andonian, Quentin Anthony, Stella Biderman, Sid Black, Preetham Gali, Leo Gao, Eric Hallahan, Josh Levy-Kramer, Connor Leahy, Lucas Nestler, Kip Parker, Michael Pieler, Shivanshu Purohit, Tri Songz, Wang Phil, and Samuel Weinbach. GPT-NeoX: Large Scale Autoregressive Language Modeling in PyTorc… [find](https://scholar.google.com/scholar?q=Alex+Andonian%2C+Quentin+Anthony%2C+Stella+Biderman%2C+Sid+Black%2C+Preetham+Gali%2C+Leo+Gao%2C+Eric+Hallahan%2C+Josh+Levy%2DKramer%2C+Connor+Leahy%2C+Lucas+Nestler%2C+Kip+Parker%2C+Michael+Pieler%2C+Shivanshu+Purohit%2C+Tri+Son)
2. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. [find](https://scholar.google.com/scholar?q=Yves+Bertot+and+Pierre+Cast%C3%A9ran%2E+Interactive+Theorem+Proving+and+Program+Development+%2D+Coq%E2%80%99Art%3A+The+Calculus+of+Inductive+Constructions%2E+Springer%2C+2004%2E)
3. Stella Biderman, Hailey Schoelkopf, Quentin Anthony, Herbie Bradley, Kyle O’Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, USVSN Sai Prashanth, Aviya Skowron, Lintang Sutawika, and Oskar van der Wal. Pythia: a scaling suite for language model interpretability research. Computing Resea… — [doi:10.48550/arxiv.2201.07311](https://doi.org/10.48550/arxiv.2201.07311) [find](https://scholar.google.com/scholar?q=Stella+Biderman%2C+Hailey+Schoelkopf%2C+Quentin+Anthony%2C+Herbie+Bradley%2C+Kyle+O%E2%80%99Brien%2C+Eric+Hallahan%2C+Mohammad+Aflah+Khan%2C+Shivanshu+Purohit%2C+USVSN+Sai+Prashanth%2C+Aviya+Skowron%2C+Lintang+Sutawika%2C+and+Oska)
4. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… [find](https://scholar.google.com/scholar?q=Tom+B%2E+Brown%2C+Benjamin+Mann%2C+Nick+Ryder%2C+Melanie+Subbiah%2C+Jared+Kaplan%2C+Prafulla+Dhariwal%2C+Arvind+Neelakantan%2C+Pranav+Shyam%2C+Girish+Sastry%2C+Amanda+Askell%2C+Sandhini+Agarwal%2C+Ariel+Herbert%2DVoss%2C+Gretche)
5. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 299–312. [find](https://scholar.google.com/scholar?q=Kevin+Buzzard%2C+Johan+Commelin%2C+and+Patrick+Massot%2E+Formalising+perfectoid+spaces%2E+In+Jasmin+Blanchette+and+Catalin+Hritcu%2C+editors%2C+Proceedings+of+the+9th+ACM+SIGPLAN+International+Conference+on+Certi)
6. ACM, 2020. doi: 10.1145/3372885.3373830. URL https://doi.org/10.1145/3372885.3373830. [↗](https://doi.org/10.1145/3372885.3373830)
7. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhai… [find](https://scholar.google.com/scholar?q=Mark+Chen%2C+Jerry+Tworek%2C+Heewoo+Jun%2C+Qiming+Yuan%2C+Henrique+Ponde+de+Oliveira+Pinto%2C+Jared+Kaplan%2C+Harri+Edwards%2C+Yuri+Burda%2C+Nicholas+Joseph%2C+Greg+Brockman%2C+Alex+Ray%2C+Raul+Puri%2C+Gretchen+Krueger%2C+Mich) [our card](https://md.research.elamur.ai/free/en/papers/chen-2021-evaluating-large-language-models-trained/)
8. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Conference on Automated Deduction (CADE) 2015, pages 378–388. [find](https://scholar.google.com/scholar?q=Leonardo+Mendon%C3%A7a+de+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+van+Doorn%2C+and+Jakob+von+Raumer%2E+The+Lean+theorem+prover+%28system+description%29%2E+In+Amy+P%2E+Felty+and+Aart+Middeldorp%2C+editors%2C+Conference+o)
9. Xavier Garcia, Yamini Bansal, Colin Cherry, George Foster, Maxim Krikun, Fangxiaoyu Feng, Melvin Johnson, and Orhan Firat. The unreasonable effectiveness of few-shot learning for machine translation, 2023. URL https://arxiv.org/abs/2302.01398. — [arXiv:2302.01398](https://arxiv.org/abs/2302.01398) [↗](https://arxiv.org/abs/2302.01398)
10. Herbert L. Gelernter. Realization of a geometry theorem proving machine. In IFIP Congress, 1959. [find](https://scholar.google.com/scholar?q=Herbert+L%2E+Gelernter%2E+Realization+of+a+geometry+theorem+proving+machine%2E+In+IFIP+Congress%2C+1959%2E)
11. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. [find](https://scholar.google.com/scholar?q=Adam+Grabowski%2C+Artur+Kornilowicz%2C+and+Adam+Naumowicz%2E+Mizar+in+a+nutshell%2E+J%2E+Formalized+Reasoning%2C+3%282%29%3A153%E2%80%93245%2C+2010%2E)
12. Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever. Unsupervised neural machine translation with generative language models only, 2021a. URL https://arxiv.org/abs/2110.05448. — [arXiv:2110.05448](https://arxiv.org/abs/2110.05448) [↗](https://arxiv.org/abs/2110.05448)
13. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models, 2021b. URL https://arxiv.org/abs/2102.06203. [↗](https://arxiv.org/abs/2102.06203)
14. 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, 2021. URL https://arxiv.org/abs/2103.03874. [↗](https://arxiv.org/abs/2103.03874) [our card](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/)
15. Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The curious case of neural text degeneration, 2019. URL https://arxiv.org/abs/1904.09751. [↗](https://arxiv.org/abs/1904.09751)
16. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath - deep sequence models for premise selection. In D. Lee, M. Sugiyama, U. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 29. Curran Ass… [find](https://scholar.google.com/scholar?q=Geoffrey+Irving%2C+Christian+Szegedy%2C+Alexander+A+Alemi%2C+Niklas+Een%2C+Francois+Chollet%2C+and+Josef+Urban%2E+Deepmath+%2D+deep+sequence+models+for+premise+selection%2E+In+D%2E+Lee%2C+M%2E+Sugiyama%2C+U%2E+Luxburg%2C+I%2E+Guyo)
17. Albert Q. 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, 2022a. URL https://arxiv.org/abs/2205.10893. [↗](https://arxiv.org/abs/2205.10893)
18. 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, 2022b. URL https://arxiv.org/abs/2210.12283. [↗](https://arxiv.org/abs/2210.12283) [our card](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/)
19. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners, 2022. URL https://arxiv.org/abs/2205.11916. [↗](https://arxiv.org/abs/2205.11916) [our card](https://md.research.elamur.ai/free/en/papers/kojima-2022-large-language-models-zero-shot/)
20. Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only, 2017. URL https://arxiv.org/abs/1711.00043. [↗](https://arxiv.org/abs/1711.00043) [our card](https://md.research.elamur.ai/free/en/papers/lample-2017-unsupervised-machine-translation-using-monolingual/)
21. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving, 2022. URL https://arxiv.org/abs/2205.11491. [↗](https://arxiv.org/abs/2205.11491) [our card](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/)
22. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models, 2022. URL https://arxiv… [find](https://scholar.google.com/scholar?q=Aitor+Lewkowycz%2C+Anders+Andreassen%2C+David+Dohan%2C+Ethan+Dyer%2C+Henryk+Michalewski%2C+Vinay+Ramasesh%2C+Ambrose+Slone%2C+Cem+Anil%2C+Imanol+Schlag%2C+Theo+Gutman%2DSolo%2C+Yuhuai+Wu%2C+Behnam+Neyshabur%2C+Guy+Gur%2DAri%2C+and) [our card](https://md.research.elamur.ai/free/en/papers/lewkowycz-2022-solving-quantitative-reasoning-problems-language/)
23. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIG-PLAN International Conference on Certified Programs and Proofs. ACM, jan 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145%2F3372885.3373824. [find](https://scholar.google.com/scholar?q=The+mathlib+Community%2E+The+lean+mathematical+library%2E+In+Proceedings+of+the+9th+ACM+SIG%2DPLAN+International+Conference+on+Certified+Programs+and+Proofs%2E+ACM%2C+jan+2020%2E+doi%3A+10%2E1145%2F3372885%2E3373824%2E+URL)
24. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002. [find](https://scholar.google.com/scholar?q=Tobias+Nipkow%2C+Lawrence+C%2E+Paulson%2C+and+Markus+Wenzel%2E+Isabelle%2FHOL+%2D+A+Proof+Assistant+for+Higher%2DOrder+Logic%2E+Springer%2C+2002%2E)
25. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002. [find](https://scholar.google.com/scholar?q=Kishore+Papineni%2C+Salim+Roukos%2C+Todd+Ward%2C+and+Wei%2DJing+Zhu%2E+Bleu%3A+a+method+for+automatic+evaluation+of+machine+translation%2E+In+Proceedings+of+the+40th+annual+meeting+of+the+Association+for+Computatio) [our card](https://md.research.elamur.ai/free/en/papers/papineni-2002-bleu-method-automatic-evaluation-machine/)
26. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020. URL https://arxiv.org/abs/2009.03393. [↗](https://arxiv.org/abs/2009.03393) [our card](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/)
27. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022. URL https://arxiv.org/abs/2202.01344. [↗](https://arxiv.org/abs/2202.01344) [our card](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/)
28. Markus N. Rabe and Christian Szegedy. Towards the automatic mathematician. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28, pages 25–37, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5. [find](https://scholar.google.com/scholar?q=Markus+N%2E+Rabe+and+Christian+Szegedy%2E+Towards+the+automatic+mathematician%2E+In+Andr%C3%A9+Platzer+and+Geoff+Sutcliffe%2C+editors%2C+Automated+Deduction+%E2%80%93+CADE+28%2C+pages+25%E2%80%9337%2C+Cham%2C+2021%2E+Springer+International)
29. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, L. Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self-play with a general reinforcement learning algorithm.… [find](https://scholar.google.com/scholar?q=David+Silver%2C+Thomas+Hubert%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Matthew+Lai%2C+Arthur+Guez%2C+Marc+Lanctot%2C+L%2E+Sifre%2C+Dharshan+Kumaran%2C+Thore+Graepel%2C+Timothy+P%2E+Lillicrap%2C+Karen+Simonyan%2C+and+Demi) [our card](https://md.research.elamur.ai/free/en/papers/al-2017-mastering-chess-shogi-self-play/)
30. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 3–20, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6. [find](https://scholar.google.com/scholar?q=Christian+Szegedy%2E+A+promising+path+towards+autoformalization+and+general+artificial+intelligence%2E+In+Christoph+Benzm%C3%BCller+and+Bruce+Miller%2C+editors%2C+Intelligent+Computer+Mathematics%2C+pages+3%E2%80%9320%2C+Cham)
31. Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Formal premise selection with language models, 2022. URL [http://aitp-conference.org/2022/abstract/AITP_2022_paper_32.pdf](http://aitp-conference.org/2022/abstract/AITP_2022_paper_32.pdf). [↗](http://aitp-conference.org/2022/abstract/AITP_2022_paper_32.pdf)
32. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, Intelligent Computer Mathematics, pages 255–270, Cham, 2018. Springer International Publis… [find](https://scholar.google.com/scholar?q=Qingxiang+Wang%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+First+experiments+with+neural+translation+of+informal+to+formal+mathematics%2E+In+Florian+Rabe%2C+William+M%2E+Farmer%2C+Grant+O%2E+Passmore%2C+and+Abdou+Youssef%2C)
33. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language, 2021. URL https://arxiv.org/abs/2104.01112. [↗](https://arxiv.org/abs/2104.01112)
34. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models, 2022. URL https://arxiv.org/abs/2205.12910. [↗](https://arxiv.org/abs/2205.12910)
35. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022a. URL https://arxiv.org/abs/2205.12615. [↗](https://arxiv.org/abs/2205.12615) [our card](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/)
36. Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In International Conference on Learning Representations, 2022b. URL [https://openreview.net/forum?id=TrjbxzRcnf-](https://openreview.net/forum?id=TrjbxzRcnf-). [↗](https://openreview.net/forum?id=TrjbxzRcnf-)
37. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019. URL https://arxiv.org/abs/1905.09381. [↗](https://arxiv.org/abs/1905.09381)
38. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. [find](https://scholar.google.com/scholar?q=Kunhao+Zheng%2C+Jesse+Michael+Han%2C+and+Stanislas+Polu%2E+minif2f%3A+a+cross%2Dsystem+benchmark+for+formal+olympiad%2Dlevel+mathematics%2E+In+The+Tenth+International+Conference+on+Learning+Representations%2C+ICLR+20) [our card](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/)
39. OpenReview.net, 2022. URL [https://openreview.net/forum?id=9ZPegFuFTFv](https://openreview.net/forum?id=9ZPegFuFTFv). [↗](https://openreview.net/forum?id=9ZPegFuFTFv)
40. Parameter Tokens Epochs Training Steps Learning Rate Max Learning Rate Min Optimizer Adam Betas Adam Eps Weight Decay LR Scheduler LR Warm-up Steps Effective Batch Size Precision Gradient Clipping Table 4: PROOF GPT training hyperparameters. [find](https://scholar.google.com/scholar?q=Parameter+Tokens+Epochs+Training+Steps+Learning+Rate+Max+Learning+Rate+Min+Optimizer+Adam+Betas+Adam+Eps+Weight+Decay+LR+Scheduler+LR+Warm%2Dup+Steps+Effective+Batch+Size+Precision+Gradient+Clipping+Tab)