SOTAVerified

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 AddedMost HypedMost ActiveNeeds VerificationMost Verified

Showing 1–10 of 288 papers

TitleStatusHype
CriticLean: Critic-Guided Reinforcement Learning for Mathematical FormalizationCode1
Prover Agent: An Agent-based Framework for Formal Mathematical Proofs—0
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving—0
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?—0
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal VerificationCode1
LeanExplore: A search engine for Lean 4 declarationsCode2
Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening—0
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations—0
ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction—0
DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement LearningCode1
Show:102550
← PrevPage 1 of 29Next →
All datasetsminiF2F-testminiF2F-validHolStep (Conditional)HOList benchmarkHolStep (Unconditional)Metamath set.mmminiF2F-curriculumCompCertCoqGym

Benchmark Results

#ModelMetricClaimedVerifiedStatus
1EvaristePass@3272.4—Unverified
2GPT-fPercentage correct56.2—Unverified
3MetaGen-IL + HolophrasmPercentage correct22.1—Unverified
4HolophrasmPercentage correct14.3—Unverified