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	Score
Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions	May 24, 2025	Automated Theorem ProvingMath	CodeCode Available	5
Solving Quantified Modal Logic Problems by Translation to Classical Logics	Dec 19, 2022	Automated Theorem ProvingTranslation	CodeCode Available	5
Learning Symbolic Rules for Reasoning in Quasi-Natural Language	Nov 23, 2021	Automated Theorem ProvingFormal Logic	CodeCode Available	5
Automated proof synthesis for propositional logic with deep neural networks	May 30, 2018	Automated Theorem Proving	CodeCode Available	5
Holophrasm: a neural Automated Theorem Prover for higher-order logic	Aug 8, 2016	Automated Theorem Proving	CodeCode Available	5
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving	Mar 1, 2017	Automated Theorem ProvingBIG-bench Machine Learning	CodeCode Available	5
HOL(y)Hammer: Online ATP Service for HOL Light	Sep 19, 2013	Automated Theorem ProvingCPU	CodeCode Available	5
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint	May 24, 2023	Automated Theorem ProvingTranslation	CodeCode Available	5
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving	Jan 22, 2024	Automated Theorem Proving	CodeCode Available	5
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving	Apr 10, 2024	Automated Theorem ProvingLanguage Modeling	CodeCode Available	5
Large Language Models' Understanding of Math: Source Criticism and Extrapolation	Nov 12, 2023	Automated Theorem ProvingMath	—Unverified	0
Deriving Theorems in Implicational Linear Logic, Declaratively	Sep 22, 2020	Automated Theorem Proving	—Unverified	0
Keyword-based Natural Language Premise Selection for an Automatic Mathematical Statement Proving	Oct 1, 2022	Automated Theorem ProvingInformation Retrieval	—Unverified	0
jsCoq: Towards Hybrid Theorem Proving Interfaces	Jan 25, 2017	Automated Theorem Proving	—Unverified	0
ATG: Benchmarking Automated Theorem Generation for Generative Language Models	May 5, 2024	Automated Theorem ProvingBenchmarking	—Unverified	0
Interactive, Intelligent Tutoring for Auxiliary Constructions in Geometry Proofs	Nov 20, 2017	Automated Theorem Proving	—Unverified	0
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data	May 23, 2024	Automated Theorem ProvingMathematical Reasoning	—Unverified	0
Improving QED-Tutrix by Automating the Generation of Proofs	Mar 5, 2018	Automated Theorem Proving	—Unverified	0
Improving Multimodal LLMs Ability In Geometry Problem Solving, Reasoning, And Multistep Scoring	Dec 1, 2024	Automated Theorem ProvingGeometry Problem Solving	—Unverified	0
HyperTree Proof Search for Neural Theorem Proving	May 23, 2022	Automated Theorem Proving	—Unverified	0
DeepAlgebra - an outline of a program	Oct 4, 2016	Automated Theorem Proving	—Unverified	0
Analysis of Algorithms and Partial Algorithms	Jan 13, 2016	Automated Theorem Proving	—Unverified	0
Activation Steering in Neural Theorem Provers	Feb 21, 2025	Automated Theorem Proving	—Unverified	0
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement	May 21, 2025	Automated Theorem ProvingMathematical Proofs	—Unverified	0
HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving	Dec 30, 2024	Automated Theorem ProvingLanguage Modeling	—Unverified	0

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