Automated Theorem Proving

The goal of Automated Theorem Proving is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated Theorem Proving is useful in a wide range of applications, including the verification and synthesis of software and hardware systems.

Source: Learning to Prove Theorems by Learning to Generate Theorems

Papers

Recently Added Most Hyped Most Active Needs Verification Most Verified

Showing 51–100 of 288 papers

Title	Date	Tasks	Status	Hype
LEGO-Prover: Neural Theorem Proving with Growing Libraries	Oct 1, 2023	Automated Theorem Proving	CodeCode Available	1
Learning as Abduction: Trainable Natural Logic Theorem Prover for Natural Language Inference	Oct 29, 2020	Automated Theorem ProvingNatural Language Inference	CodeCode Available	1
Beyond Autoregression: Fast LLMs via Self-Distillation Through Time	Oct 28, 2024	Automated Theorem ProvingCode Generation	CodeCode Available	1
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving	May 25, 2023	Automated Theorem Proving	CodeCode Available	1
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving	Nov 5, 2019	Automated Theorem ProvingDeep Reinforcement Learning	CodeCode Available	1
Linear algebra with transformers	Dec 3, 2021	Automated Theorem ProvingFew-Shot Learning	CodeCode Available	1
Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis	Jan 30, 2025	Automated Theorem ProvingMath	CodeCode Available	1
LeanReasoner: Boosting Complex Logical Reasoning with Lean	Mar 20, 2024	Automated Theorem ProvingLogical Reasoning	CodeCode Available	1
LangPro: Natural Language Theorem Prover	Aug 30, 2017	Automated Theorem ProvingNatural Language Inference	CodeCode Available	1
Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization	Mar 26, 2024	Automated Theorem ProvingGSM8K	CodeCode Available	1
An energy-based model for neuro-symbolic reasoning on knowledge graphs	Oct 4, 2021	Automated Theorem ProvingGraph Embedding	CodeCode Available	1
Leanabell-Prover: Posttraining Scaling in Formal Reasoning	Apr 8, 2025	Automated Theorem Provingreinforcement-learning	CodeCode Available	1
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics	Aug 31, 2021	Automated Theorem Proving	CodeCode Available	1
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics	Feb 24, 2023	Abstract AlgebraAutomated Theorem Proving	CodeCode Available	1
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs	Oct 21, 2022	Automated Theorem ProvingLanguage Modeling	CodeCode Available	1
Deriving Theorems in Implicational Linear Logic, Declaratively	Sep 22, 2020	Automated Theorem Proving	—Unverified	0
ATG: Benchmarking Automated Theorem Generation for Generative Language Models	May 5, 2024	Automated Theorem ProvingBenchmarking	—Unverified	0
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data	May 23, 2024	Automated Theorem ProvingMathematical Reasoning	—Unverified	0
Analysis of Algorithms and Partial Algorithms	Jan 13, 2016	Automated Theorem Proving	—Unverified	0
Improving QED-Tutrix by Automating the Generation of Proofs	Mar 5, 2018	Automated Theorem Proving	—Unverified	0
DeepAlgebra - an outline of a program	Oct 4, 2016	Automated Theorem Proving	—Unverified	0
Activation Steering in Neural Theorem Provers	Feb 21, 2025	Automated Theorem Proving	—Unverified	0
CSPLib: Twenty Years On	Sep 30, 2019	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified	0
A Study of Continuous Vector Representationsfor Theorem Proving	Jan 22, 2021	Automated Theorem Proving	—Unverified	0
Cross-checking WordNet and SUMO Using Meronymy	May 1, 2018	Automated Theorem Proving	—Unverified	0
A state vector algebra for algorithmic implementation of second-order logic	Dec 9, 2013	Automated Theorem Proving	—Unverified	0
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation	Feb 25, 2025	Automated Theorem ProvingLanguage Modeling	—Unverified	0
COVER: Covering the Semantically Tractable Questions	Apr 1, 2017	Automated Theorem ProvingSemantic Parsing	—Unverified	0
Count-Invariance Including Exponentials	Jul 1, 2017	Automated Theorem Proving	—Unverified	0
Artificial Neural Networks that Learn to Satisfy Logic Constraints	Dec 8, 2017	Automated Theorem Proving	—Unverified	0
Constrained Training of Neural Networks via Theorem Proving	Jul 8, 2022	Automated Theorem ProvingCode Generation	—Unverified	0
GeoGebra Tools with Proof Capabilities	Mar 3, 2016	Automated Theorem ProvingBenchmarking	—Unverified	0
Consistent CCG Parsing over Multiple Sentences for Improved Logical Reasoning	Apr 19, 2018	Automated Theorem ProvingFormal Logic	—Unverified	0
Artifical intelligence and inherent mathematical difficulty	Aug 1, 2024	Automated Theorem Proving	—Unverified	0
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes	Oct 14, 2024	Automated Theorem ProvingDiversity	—Unverified	0
Conjectures, Tests and Proofs: An Overview of Theory Exploration	Sep 7, 2021	Automated Theorem ProvingMathematical Reasoning	—Unverified	0
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving	Sep 26, 2022	Automated Theorem Proving	—Unverified	0
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective	Jan 19, 2025	Automated Theorem ProvingMath	—Unverified	0
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof	Oct 21, 2021	Automated Theorem Proving	—Unverified	0
A Certified Proof Checker for Deep Neural Network Verification in Imandra	May 17, 2024	Automated Theorem ProvingLEMMA	—Unverified	0
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)	Jul 18, 2022	Automated Theorem Proving	—Unverified	0
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs	Feb 16, 2025	Automated Theorem ProvingMathematical Proofs	—Unverified	0
Generative Language Modeling for Automated Theorem Proving	Sep 7, 2020	Automated Theorem ProvingLanguage Modeling	—Unverified	0
Generative Learning of Continuous Data by Tensor Networks	Oct 31, 2023	Automated Theorem ProvingTensor Networks	—Unverified	0
0-1 laws for pattern occurrences in phylogenetic trees and networks	Feb 7, 2024	10-shot image generation	—Unverified	0
Can neural networks do arithmetic? A survey on the elementary numerical skills of state-of-the-art deep learning models	Mar 14, 2023	Automated Theorem ProvingDeep Learning	—Unverified	0
GraATP: A Graph Theoretic Approach for Automated Theorem Proving in Plane Geometry	Dec 18, 2014	Automated Theorem Proving	—Unverified	0
Graph2Tac: Online Representation Learning of Formal Math Concepts	Jan 5, 2024	AI AgentAutomated Theorem Proving	—Unverified	0
Graph Contrastive Pre-training for Effective Theorem Reasoning	Aug 24, 2021	Automated Theorem ProvingContrastive Learning	—Unverified	0
From Width-Based Model Checking to Width-Based Automated Theorem Proving	May 23, 2022	Automated Theorem Provingvalid	—Unverified	0

Show:10 25 50

← PrevPage 2 of 6Next →

All datasets miniF2F-test miniF2F-valid HolStep (Conditional)HOList benchmark HolStep (Unconditional)Metamath set.mm miniF2F-curriculum CompCert CoqGym

Benchmark Results

#	Model	Metric	Claimed	Verified	Status
1	Kimina-Prover-Preview	cumulative	80.74	—	Unverified
2	ProofAug	cumulative	66	—	Unverified
3	DeepSeek-Prover-V1.5	cumulative	63.5	—	Unverified
4	Subgoal-XL	cumulative	56.1	—	Unverified
5	DeepSeek-Prover	cumulative	52	—	Unverified
6	Lyra + GPT-4	cumulative	47.1	—	Unverified
7	LEGO-Prover ChatGPT	cumulative	47.1	—	Unverified
8	Decomposing the Enigma	cumulative	45.5	—	Unverified
9	Evariste	cumulative	41	—	Unverified
10	Evariste-7d	cumulative	40.6	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste	Pass@64	58.6	—	Unverified
2	LEGO-Prover ChatGPT	Pass@100	57	—	Unverified
3	Lyra + GPT-4	Pass@100	52	—	Unverified
4	Evariste-7d	Pass@64	47.5	—	Unverified
5	GPT-f	Pass@64	47.3	—	Unverified
6	Evariste-1d	Pass@64	46.7	—	Unverified
7	DSP (62B Minerva informal)	Pass@100	43.9	—	Unverified
8	Lean GPT-f	Pass@8	29.3	—	Unverified
9	Lean tidy	Pass@1	16.8	—	Unverified
10	Metamath GPT-f	Pass@8	2	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	MPNN-DagLSTM	Classification Accuracy	0.92	—	Unverified
2	FormulaNet	Classification Accuracy	0.9	—	Unverified
3	FormulaNet-basic	Classification Accuracy	0.89	—	Unverified
4	Siamese 1D CNN-LSTM	Classification Accuracy	0.83	—	Unverified
5	Siamese 1D CNN	Classification Accuracy	0.82	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	4-hop GNN, sub-expression sharing	Percentage correct	49.95	—	Unverified
2	Tactic Dependent Loop	Percentage correct	38.88	—	Unverified
3	BoW2 (extra -ves)	Percentage correct	36.55	—	Unverified
4	Deeper Wider WaveNet	Percentage correct	32.65	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	FormulaNet	Classification Accuracy	0.9	—	Unverified
2	FormulaNet-basic	Classification Accuracy	0.89	—	Unverified
3	1D CNN-LSTM	Classification Accuracy	0.83	—	Unverified
4	1D CNN	Classification Accuracy	0.83	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste	Pass@32	72.4	—	Unverified
2	GPT-f	Percentage correct	56.2	—	Unverified
3	MetaGen-IL + Holophrasm	Percentage correct	22.1	—	Unverified
4	Holophrasm	Percentage correct	14.3	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste-7d	Pass@64	42.5	—	Unverified
2	Evariste-1d	Pass@64	33.6	—	Unverified
3	Evariste	Pass@64	32.1	—	Unverified
4	GPT-f	Pass@64	30.6	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Proverbot9001	Percentage correct	19.36	—	Unverified
2	CoqGym/ASTactic	Percentage correct	4.99	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	ASTactic	Percentage correct	12.2	—	Unverified