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 101–125 of 288 papers

Title	Date	Tasks	Status
COVER: Covering the Semantically Tractable Questions	Apr 1, 2017	Automated Theorem ProvingSemantic Parsing	—Unverified
Hammering Mizar by Learning Clause Guidance	Apr 2, 2019	Automated Theorem Proving	—Unverified
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving	Sep 26, 2022	Automated Theorem Proving	—Unverified
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective	Jan 19, 2025	Automated Theorem ProvingMath	—Unverified
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof	Oct 21, 2021	Automated Theorem Proving	—Unverified
Lean-STaR: Learning to Interleave Thinking and Proving	Jul 14, 2024	Automated Theorem ProvingLanguage Modeling	—Unverified
CSPLib: Twenty Years On	Sep 30, 2019	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified
Hua-Chen New Theory of Economic Optimization	Apr 27, 2025	Automated Theorem ProvingSurvey	—Unverified
A Certified Proof Checker for Deep Neural Network Verification in Imandra	May 17, 2024	Automated Theorem ProvingLEMMA	—Unverified
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement	May 21, 2025	Automated Theorem ProvingMathematical Proofs	—Unverified
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)	Jul 18, 2022	Automated Theorem Proving	—Unverified
HyperTree Proof Search for Neural Theorem Proving	May 23, 2022	Automated Theorem Proving	—Unverified
Improving Multimodal LLMs Ability In Geometry Problem Solving, Reasoning, And Multistep Scoring	Dec 1, 2024	Automated Theorem ProvingGeometry Problem Solving	—Unverified
Improving QED-Tutrix by Automating the Generation of Proofs	Mar 5, 2018	Automated Theorem Proving	—Unverified
0-1 laws for pattern occurrences in phylogenetic trees and networks	Feb 7, 2024	10-shot image generation	—Unverified
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
From Width-Based Model Checking to Width-Based Automated Theorem Proving	May 23, 2022	Automated Theorem Provingvalid	—Unverified
Interactive, Intelligent Tutoring for Auxiliary Constructions in Geometry Proofs	Nov 20, 2017	Automated Theorem Proving	—Unverified
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning	May 9, 2025	Automated Theorem Proving	—Unverified
From the String Landscape to the Mathematical Landscape: a Machine-Learning Outlook	Feb 12, 2022	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically	Nov 4, 2024	Automated Theorem Proving	—Unverified
Blocking and Other Enhancements for Bottom-Up Model Generation Methods	Nov 28, 2016	Automated Theorem ProvingBlocking	—Unverified
Formal Specifications from Natural Language	Jun 4, 2022	Automated Theorem Proving	—Unverified
BliStrTune: Hierarchical Invention of Theorem Proving Strategies	Nov 26, 2016	Automated Theorem Proving	—Unverified
Adversarial Learning to Reason in an Arbitrary Logic	Apr 6, 2022	Automated Theorem Proving	—Unverified

Show:10 25 50

← PrevPage 5 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