====== Automatic Theorem Proving ======

===== Overviews =====
  * [[https://arxiv.org/pdf/2205.15231.pdf|Jordan Meadows & André Freitas 2022 - A Survey in Mathematical Language Processing]]
  * **[[https://arxiv.org/pdf/2212.10535.pdf|Lu et al 2022 - A Survey of Deep Learning for Mathematical Reasoning]]**
  * **[[https://arxiv.org/pdf/2404.09939|Li et al 2024 - Survey on Deep Learning for Theorem Proving]]**
  * Formalizing mathematics
    * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/ckfr-cicm20.pdf|Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics]]
  * Autoformalization
    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]

===== Papers =====
  * [[http://ceur-ws.org/Vol-448/paper10.pdf|Cramer et al 2009 - The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts]]
  * [[https://arxiv.org/pdf/1211.7012.pdf|Kaliszyk et al 2013 - Learning-Assisted Automated Reasoning with Flyspeck]]
  * [[https://arxiv.org/pdf/1606.04442.pdf|Alemi et al 2016 - DeepMath - Deep Sequence Models for Premise Selection]]
  * [[https://arxiv.org/pdf/1703.00426.pdf|Kaliszyk et al 2017 - HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving]]
  * [[https://openreview.net/pdf?id=K5j7D81ABvt|Müller & Kaliszyk 2021 - Disambiguating Symbolic Expressions in Informal Documents]]
  * [[https://arxiv.org/pdf/2104.01112.pdf|Welleck et al 2021 - NaturalProofs: Mathematical Theorem Proving in Natural Language]] [[https://github.com/wellecks/naturalproofs|Dataset]]
  * [[https://arxiv.org/pdf/2205.12910.pdf|Welleck et al 2022 - NaturalProver: Grounded Mathematical Proof Generation with Language Models]]

==== Neural Theorem Proving ====
  * **Overviews**
    * [[https://arxiv.org/pdf/2404.09939|Li et al 2024 - A Survey on Deep Learning for Theorem Proving]]
  * **Bibliographies**
    * [[https://github.com/zhaoyu-li/DL4TP|Deep Learning for Theorem Proving (DL4TP)]]
  * **Step-by-step Proof Generation**
    * GPT-f: [[https://arxiv.org/pdf/2009.03393|Polu & Sutskever 2020 - Generative Language Modeling for Automated Theorem Proving]] Maintains a proof tree with a queue of open goals, and tries to expand the goal with the highest LLM logprob to reach it. Metamath formalization language. Introduces WebMath pre-training.
    * [[https://arxiv.org/pdf/2102.06203|Han et al 2021 - Proof Artifact Co-training for Theorem Proving with Language Models]] Generates the next tactic using an LLM. Uses a best-first search algorithm: maintains a priority queue of search nodes, of tactic state (partial proof) and metadata, sorted by LLM heuristic score.  For Lean.  Introduces the LeanStep dataset to to predict the next tactic give a goal state, built from mathlib.  Uses an interesting PACT pretraining dataset (sec 3.2).
    * [[https://aitp-conference.org/2021/abstract/paper_17.pdf|Jiang et al 2021 - LISA: Language models of ISAbelle proofs]]
    * [[https://arxiv.org/pdf/2202.01344.pdf|Polu et al 2022 - Formal Mathematics Statement Curriculum Learning]]
    * [[https://arxiv.org/pdf/2205.10893|Jiang et al 2022 - Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers]] Uses automated theorem prover premise selection (hammers) to retrieve the relevant premises, and then uses LLMs as in GPT-f ([[https://arxiv.org/pdf/2009.03393|Polu & Sutskever 2020]]).  Increases success rate on PISA from 39.0% to 57.0%.
    * [[https://arxiv.org/pdf/2205.11491|Lample et al 2022 - HyperTree Proof Search for Neural Theorem Proving]]
    * [[https://arxiv.org/pdf/2306.15626|Yang et al 2023 - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models]]
    * [[https://aclanthology.org/2023.acl-long.706.pdf|Wang et al 2023 - DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function]]
    * [[https://arxiv.org/pdf/2310.00656|Wang et al 2023 - LEGO-Prover: Neural Theorem Proving with Growing Libraries]]
    * [[https://mathai2023.github.io/papers/29.pdf|Thakur et al 2023 - A Language-Agent Approach to Formal Theorem-Proving]]
    * [[https://arxiv.org/pdf/2405.14414|Wang et al 2024 - Proving Theorems Recursively]]
  * **Construction All-In-One Go**
    * [[https://arxiv.org/pdf/2210.12283|Jiang et al 2022 - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs]]
    * [[https://arxiv.org/pdf/2305.16366|Zhao et al 2023 - Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving]]
    * [[https://arxiv.org/pdf/2303.04910|First et al 2023 - Baldur: Whole-Proof Generation and Repair with Large Language Models]]
  * [[https://arxiv.org/pdf/2310.18457|Welleck & Saha 2023 - LLMSTEP: LLM proofstep suggestions in Lean]]
  * [[https://arxiv.org/pdf/2412.20735|Li et al 2024 - HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving]]
  * [[https://arxiv.org/pdf/2502.00212|Dong & Ma 2025 - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving]]
  * [[https://arxiv.org/pdf/2505.20613|Shen et al 2025 - REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning]]


===== Formal Automated Theorem Proving =====

=== Systems ===
  * Vampire
    * [[http://www.cse.chalmers.se/~laurako/pub/CAV13_Kovacs.pdf|Kovacs & Voronkov 2013 - First-Order Theorem Proving and VAMPIRE]] Intro to VAMPIRE
    * [[https://easychair.org/publications/open/1DlL|Reger 2016 - Better Proof Output for Vampire]]
  * For Mizar dataset
    * [[https://arxiv.org/pdf/1310.2805.pdf|Kaliszyk et al 2013 - MizAR 40 for Mizar 40]] Uses Vampire, Epar, and Z3 solvers.
    * [[https://arxiv.org/pdf/2102.03529.pdf|Suda 2021 - Vampire With a Brain Is a Good ITP Hammer]] [[https://github.com/quickbeam123/deepire3.1|github]]
  * For Lean
    * Lean-Step: [[https://arxiv.org/pdf/2102.06203.pdf|Han et al 2021 - Proof Artifact Co-training for Theorem Proving with Language Models]]
  * HOL Light
    * HOList and DeepHOL: [[https://arxiv.org/pdf/1904.03241.pdf|Bansal et al 2019 - HOList: An Environment for Machine Learning of Higher-Order Theorem Proving]]

=== Datasets ===
  * [[https://www.tptp.org/|TPTP]] (Thousands of Problems for Theorem Provers [[https://www.tptp.org/TPTP/QuickGuide/|QuickGuide]] [[https://www.tptp.org/TPTP/QuickGuide/Problems.html|TPTP Format]]
  * Mizar
    * MPTP
      * Paper: [[http://ceur-ws.org/Vol-418/paper1.pdf|Urban 2008 - Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange]]
      * Dataset: [[https://github.com/JUrban/MPTP2|v2 github]] [[https://github.com/JUrban/MPTP|v1 github]]
    * MizarTPTP
      * Paper: [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.2087&rep=rep1&type=pdf|Urban et al 2007 - Combining Mizar and TPTP Semantic Presentation Tools]] {{papers:combining_mizar_and_tptp_semantic_presentation_and_verification_tools.pdf|pdf}}
      * Dataset: [[https://www.tptp.org/MizarTPTP/|website]]
  * [[https://arxiv.org/pdf/2407.11214|Tsoukalas et al 2024 - PUTNAMBENCH: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition]]

===== Formalizing Mathematics =====
  * Overviews
    * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/ckfr-cicm20.pdf|Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics]]
  * Mizar
    * {{papers:An Overview of the Mizar Project.pdf|Rudnicki 1992 - An Overview of the Mizar Project}}
    * [[https://jfr.unibo.it/article/view/1980|Grabowski et al 2010 - Mizar in a Nutshell]] {{papers:mizar_in_a_nutshell.pdf|pdf}}
    * [[https://link.springer.com/content/pdf/10.1007/11618027_23.pdf|Urban 2006 - XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy]] See also [[https://drops.dagstuhl.de/opus/volltexte/2021/13906/pdf/LIPIcs-ITP-2021-11.pdf|Byliński 2021]]. Cited by [[http://ceur-ws.org/Vol-418/paper1.pdf|Urban 2008]].
    * **[[https://drops.dagstuhl.de/opus/volltexte/2021/13906/pdf/LIPIcs-ITP-2021-11.pdf|Byliński et al 2021 - Syntactic-Semantic Form of Mizar Articles]]** Gives an overview and a good historical introduction in the intro.
    * [[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.368.286&rep=rep1&type=pdf|Grzegorz Bancerek 2006 - Automatic Translation in Formalized Mathematics]]

===== Autoformalization =====
  * Overviews
    * [[https://leanprover.zulipchat.com/user_uploads/3121/lWKHE1MCcJ1ZwiF2poPoJckC/Autoformalization.pdf|Szegedy 2019 - A Promising Path Towards Autoformalization and General Artificial Intelligence]] Great
    * [[https://arxiv.org/pdf/2311.00007|Avigad et al 2023 - Mathematics and the Formal Turn]] Great overview of the reasons to autoformalize mathematics
    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]

=== Informal Math to Formal Math Parsing ===
  * For Mizar dataset
    * [[https://arxiv.org/pdf/1405.3451.pdf|Kaliszyk et al 2014 - Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description]]
    * [[https://arxiv.org/pdf/1805.06502.pdf|Wang et al 2018 - First Experiments with Neural Translation of Informal to Formal Mathematics]] Automatic translation of informal mathematical statements in latex to formal Mizar statements. Uses a synthetically constructed dataset.
    * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/qwcbckju-cpp20.pdf|Wang et al 2020 - Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar]] Automatic translation of informal mathematical statements in latex to formal Mizar statements. Uses a synthetically constructed dataset.
  * For Isabelle
    *[[https://arxiv.org/pdf/2006.09265.pdf|Li et al 2021 - IsarStep: a Benchmark for High-level Mathematical Reasoning]] [[https://github.com/Wenda302/IsarStep|github]] Fill in a missing intermediate proposition given surrounding proofs.
    *[[https://arxiv.org/pdf/2205.12615.pdf|Wu et al 2022 - Autoformalization with Large Language Models]]


===== Automatic Premise Selection =====
  * [[https://aclanthology.org/2020.acl-main.657.pdf|Ferreira & Freitas 2020 - Premise Selection in Natural Language Mathematical Texts]]
  * [[https://arxiv.org/pdf/2310.16005.pdf|Bauer et al. 2023 - MLFMF: Data Sets for Machine Learning for
Mathematical Formalization]]
===== Software =====
  * [[https://en.wikipedia.org/wiki/Vampire_(theorem_prover)|VAMPIRE]] [[https://vprover.github.io/|website]] [[https://github.com/vprover/vampire|github]]
  * [[https://github.com/digama0/mizar-rs|Mizar proof checker]] Open-source reimplementation of the Mizar proof checker
    * Tutorial paper: [[http://www.cse.chalmers.se/~laurako/pub/CAV13_Kovacs.pdf|Kovacs & Voronkov 2013 - First-Order Theorem Proving and VAMPIRE]]
    * CMU slides: [[http://www.cs.cmu.edu/~emc/15817-s12/lecture/20120425_vampire.pdf|Vampire]]
    * Lecture: [[http://fmv.jku.at/rerise14/rerise14-fo-slides.pdf|slides]]
  * Mizar (miscellaneous software)
    * [[https://github.com/jessealama/tptp4mizar|tptp4mizar]]: Generating Mizar texts from TPTP problems and solutions
    * Generate Latex files from Mizar articles: 
      * [[https://link.springer.com/chapter/10.1007/978-3-319-96812-4_1|System Description: XSL-Based Translator of Mizar to LaTeX]]
      * [[https://cicm-conference.org/2018/slides/T23.pdf|Slides]]
      * [[https://github.com/JUrban/mizarmode/blob/master/mizar.el|Emacs Lisp mode for Mizar]]
      * [[http://jurban.github.io/mizarmode/doc/html/MizarMode.html|Mizar Mode Documentation]]

===== Courses and Tutorials =====
  * Automated Theorem Proving (in general)
    * [[http://cl-informatik.uibk.ac.at/teaching/ss22/itpThy/introduction.php|Interactive Theorem Proving @ Innsbruck]]
  * Mizar
    * [[http://mizar.org/cicm_tutorial/mizar.pdf|Tutorial]] Good tutorial, use along with [[https://jfr.unibo.it/article/view/1980|Mizar in a Nutshell]] and [[http://mizar.org/project/mizarintro.pdf|Mizar: An Impression]] (see also recommended reading at the end of the tutorial)
    * [[http://mizar.org/project/mizman.pdf|Writing a Mizar Article in Nine Easy Steps]]
    * [[http://alioth.uwb.edu.pl/~adamn/tphols2009_slides.pdf|A Brief Overview of Mizar (2009 slides)]]
    * [[http://mizar.org/project/bonarska91.pdf|Bonarska 1991 - An Introduction to PC Mizar]]
    * [[http://mizar.org/project/bibliography.html|Mizar Bibliography]]
  * Lean
    * [[https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/|Natural Number Game]] Intro to Lean (great).  [[https://www.youtube.com/watch?v=tJtUW1bQ83s|Youtube video]]
    * Lean for the Curious Mathematician [[https://icerm.brown.edu/topical_workshops/tw-22-lean/|2022]] [[https://lftcm2023.github.io/|2023]] (Workshop) Has videos
    * Learning Lean
      * [[https://leanprover-community.github.io/learn.html|Learning Lean 4]] - List of places to learn
      * **[[https://lean-lang.org/theorem_proving_in_lean/index.html|A glimpse of Lean]]** - Fast paced, for mathematicians
      * **Mathematics in Lean: [[https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf|pdf]] [[https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html|online]]** Good place to start for a mathematician
      * [[https://lean-lang.org/theorem_proving_in_lean4/|Theorem Proving in Lean 4]] [[https://lean-lang.org/theorem_proving_in_lean/index.html|Lean 3 version]] - Jeff can't stand this book


===== Workshops and Conferences =====
  * See [[https://leanprover-community.github.io/events.html|Lean-related conferences and events]]

===== People =====
  * [[https://www.andrew.cmu.edu/user/avigad/papers.html|Jeremy Avigad]]
  * [[https://scholar.google.com/citations?user=bp68Q1kAAAAJ&hl=en|Cezary Kaliszyk]] [[http://cl-informatik.uibk.ac.at/users/cek/|homepage]]
  * [[https://scholar.google.com/citations?user=3QeF7mAAAAAJ&hl=en|Christian Szegedy]] (at Google)
  * [[https://scholar.google.com/citations?user=bOQGfFIAAAAJ&hl=en|Yuhuai Wu]] (at Google)
  * [[https://www.cl.cam.ac.uk/~wl302/|Wenda Li]]
  * [[https://jasonrute.github.io/|Jason Rute]]
===== Related Pages =====
  * [[nlp:Controlled Language]]
  * [[nlp:Logic in NLP]]
  * [[nlp:NLP for Math]]