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 126–150 of 288 papers

Title	Date	Tasks	Status
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective	Jan 19, 2025	Automated Theorem ProvingMath	—Unverified
Conjectures, Tests and Proofs: An Overview of Theory Exploration	Sep 7, 2021	Automated Theorem ProvingMathematical Reasoning	—Unverified
Consistent CCG Parsing over Multiple Sentences for Improved Logical Reasoning	Apr 19, 2018	Automated Theorem ProvingFormal Logic	—Unverified
Constrained Training of Neural Networks via Theorem Proving	Jul 8, 2022	Automated Theorem ProvingCode Generation	—Unverified
Count-Invariance Including Exponentials	Jul 1, 2017	Automated Theorem Proving	—Unverified
COVER: Covering the Semantically Tractable Questions	Apr 1, 2017	Automated Theorem ProvingSemantic Parsing	—Unverified
Cross-checking WordNet and SUMO Using Meronymy	May 1, 2018	Automated Theorem Proving	—Unverified
CSPLib: Twenty Years On	Sep 30, 2019	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified
DeepAlgebra - an outline of a program	Oct 4, 2016	Automated Theorem Proving	—Unverified
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data	May 23, 2024	Automated Theorem ProvingMathematical Reasoning	—Unverified
Deriving Theorems in Implicational Linear Logic, Declaratively	Sep 22, 2020	Automated Theorem Proving	—Unverified
Designing Game of Theorems	Jun 20, 2019	Automated Theorem ProvingGame of Go	—Unverified
Efficient Neural Clause-Selection Reinforcement	Mar 10, 2025	Automated Theorem ProvingCPU	—Unverified
Modelling Value-oriented Legal Reasoning in LogiKEy	Jun 23, 2020	Automated Theorem ProvingLegal Reasoning	—Unverified
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code	Mar 19, 2024	Automated Theorem ProvingCode Generation	—Unverified
Enhancing Mathematical Reasoning in Large Language Models with Self-Consistency-Based Hallucination Detection	Apr 13, 2025	Answer SelectionAutomated Theorem Proving	—Unverified
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method	Dec 20, 2023	Automated Theorem ProvingData Augmentation	—Unverified
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E	Mar 7, 2019	Automated Theorem Proving	—Unverified
EuclidNet: Deep Visual Reasoning for Constructible Problems in Geometry	Dec 27, 2022	Automated Theorem ProvingVisual Reasoning	—Unverified
Evaluating an Automata Approach to Query Containment	Sep 1, 2017	Automated Theorem ProvingText Generation	—Unverified
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages	Feb 12, 2024	Automated Theorem ProvingBenchmarking	—Unverified
Exploring Length Generalization in Large Language Models	Jul 11, 2022	Automated Theorem ProvingIn-Context Learning	—Unverified
Extracting Higher-Order Goals from the Mizar Mathematical Library	May 23, 2016	ArticlesAutomated Theorem Proving	—Unverified
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations	May 30, 2025	Automated Theorem ProvingNatural Language Inference	—Unverified
Faithful Logic Embeddings in HOL -- Deep and Shallow	Feb 26, 2025	AllAutomated Theorem Proving	—Unverified

Show:10 25 50

← PrevPage 6 of 12Next →

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	Classification Accuracy	0.83	—	Unverified
4	1D CNN-LSTM	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