Automatic Theorem Proving

Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics

Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey

Li et al 2024 - A Survey on Deep Learning for Theorem Proving

Deep Learning for Theorem Proving (DL4TP)

GPT-f: 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.

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

Jiang et al 2021 - LISA: Language models of ISAbelle proofs

Polu et al 2022 - Formal Mathematics Statement Curriculum Learning

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 (Polu & Sutskever 2020). Increases success rate on PISA from 39.0% to 57.0%.

Lample et al 2022 - HyperTree Proof Search for Neural Theorem Proving

Yang et al 2023 - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Wang et al 2023 - DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function

Wang et al 2023 - LEGO-Prover: Neural Theorem Proving with Growing Libraries

Thakur et al 2023 - A Language-Agent Approach to Formal Theorem-Proving

Wang et al 2024 - Proving Theorems Recursively

Jiang et al 2022 - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

Zhao et al 2023 - Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

First et al 2023 - Baldur: Whole-Proof Generation and Repair with Large Language Models

Kovacs & Voronkov 2013 - First-Order Theorem Proving and VAMPIRE Intro to VAMPIRE

Reger 2016 - Better Proof Output for Vampire

Kaliszyk et al 2013 - MizAR 40 for Mizar 40 Uses Vampire, Epar, and Z3 solvers.

Suda 2021 - Vampire With a Brain Is a Good ITP Hammer github

Lean-Step: Han et al 2021 - Proof Artifact Co-training for Theorem Proving with Language Models

HOList and DeepHOL: Bansal et al 2019 - HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics

Rudnicki 1992 - An Overview of the Mizar Project

Grabowski et al 2010 - Mizar in a Nutshell pdf

Urban 2006 - XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy See also Byliński 2021. Cited by Urban 2008.

Byliński et al 2021 - Syntactic-Semantic Form of Mizar Articles Gives an overview and a good historical introduction in the intro.

Grzegorz Bancerek 2006 - Automatic Translation in Formalized Mathematics

Szegedy 2019 - A Promising Path Towards Autoformalization and General Artificial Intelligence Great

Avigad et al 2023 - Mathematics and the Formal Turn Great overview of the reasons to autoformalize mathematics

Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey

Kaliszyk et al 2014 - Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description

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.

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.

Li et al 2021 - IsarStep: a Benchmark for High-level Mathematical Reasoning github Fill in a missing intermediate proposition given surrounding proofs.

Tutorial paper: Kovacs & Voronkov 2013 - First-Order Theorem Proving and VAMPIRE

CMU slides: Vampire

Lecture: slides

tptp4mizar: Generating Mizar texts from TPTP problems and solutions

Interactive Theorem Proving @ Innsbruck

Tutorial Good tutorial, use along with Mizar in a Nutshell and Mizar: An Impression (see also recommended reading at the end of the tutorial)

Writing a Mizar Article in Nine Easy Steps

A Brief Overview of Mizar (2009 slides)

Bonarska 1991 - An Introduction to PC Mizar

Mizar Bibliography

Natural Number Game Intro to Lean (great). Youtube video

Lean for the Curious Mathematician 2022 2023 (Workshop) Has videos