TheoremBench is a Lean4 benchmark of classical theorems in main and premised forms that evaluates LLM provers on partial progress, coverage, and token efficiency rather than binary success on competition problems.
hub Canonical reference
Generative Language Modeling for Automated Theorem Proving
Canonical reference. 80% of citing Pith papers cite this work as background.
51
Pith papers citing it
44
external citations · Pith
Background
80% of classified citations
abstract
We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original mathematical terms -- might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.
hub tools
citation-role summary
background 4
method 1
citation-polarity summary
representative citing papers
A general LLM code agent paired with a Coq verification harness automatically proves all 4,257 Iris separation logic lemmas and 318 reglang lemmas with zero failures.
LAMP achieves 96.7% success generating verified Lean proofs for 90 Combinatorics on Words theorems by coordinating Planner, Builder, and Verifier agents with a CoW ontology accessed through Model Context Protocol.
Proofs depending on the axiom of choice show a geometric signature in neural embeddings of tactic sequences that weakens with dependency-graph distance and correlates with prover failure rates.
CrypFormBench is a new benchmark jointly covering symbolic and computational security to evaluate LLMs on five formal analysis capabilities, with results showing top model Claude-3.5 scores 48.7/100 and most models struggling on generation, transformation, and correction.
TheoremGraph builds a unified statement-level dependency graph across informal arXiv math and formal Lean code via parsing, embeddings, and LLM validation, releasing the data and APIs for search and retrieval.
Fine-tuned 0.6B LLMs with beam search achieve 85% success on 60 test Shannon entropy inequalities (n=10-15), outperforming GPT-5.5 (1.7%) and Psitip (33.3%).
LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
An RL-guided MCTS proof search for Tamarin finds more and shorter proofs than standard search across 16 protocol models.
An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.
Introduces rewriting categories to formalize proof equivariance and success invariance, shows LLM provers violate both, and demonstrates test-time aggregation recovers invariance and boosts performance.
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
ABD benchmark evaluates LLMs on producing parsimonious first-order exception formulas in three observation regimes using SMT verification, finding high validity but persistent parsimony and generalization gaps.
Massive activations are constant large values in LLMs that function as indispensable bias terms and concentrate attention probabilities on specific tokens.
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.
OrthoReg penalizes overlap between symbolic and neural components in hybrid dynamical models, improving symbolic recovery and out-of-distribution behavior under partial library mismatch.
VERITAS improves zero-shot formal theorem proving to 40.6% on miniF2F and 7.3% on a new combinatorics benchmark by routing verifier signals into a two-phase Best-of-N then critic-guided MCTS protocol.
A proxy-judge framework for autoformalization organizes checks into three structural scopes to produce a verdict vector that drives targeted refinement, with geometric contraction of the intrinsic gap under bounded judge noise.
EVA extracts continuous expected values from discrete token distributions in generative reward models via auxiliary MSE loss, instantiated as Leibniz for Lean 4 formal verification.
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
ImProver 2 combines a data-efficient expert-iteration pipeline with a neurosymbolic scaffold to train a 7B model that outperforms larger models in Lean 4 proof optimization across structural metrics.
RMA, a multi-agent system with structured memory and iterative feedback loops, solves 8 out of 10 research-level math problems on the new First Proof benchmark and outperforms GPT-5.2R and Aletheia according to expert evaluation.
citing papers explorer
-
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
TheoremBench is a Lean4 benchmark of classical theorems in main and premised forms that evaluates LLM provers on partial progress, coverage, and token efficiency rather than binary success on competition problems.
-
Harnessing Code Agents for Automatic Software Verification
A general LLM code agent paired with a Coq verification harness automatically proves all 4,257 Iris separation logic lemmas and 318 reglang lemmas with zero failures.
-
LAMP: Lean-based Agentic framework with MCP and Proof Repair
LAMP achieves 96.7% success generating verified Lean proofs for 90 Combinatorics on Words theorems by coordinating Planner, Builder, and Verifier agents with a CoW ontology accessed through Model Context Protocol.
-
Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
Proofs depending on the axiom of choice show a geometric signature in neural embeddings of tactic sequences that weakens with dependency-graph distance and correlates with prover failure rates.
-
CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
CrypFormBench is a new benchmark jointly covering symbolic and computational security to evaluate LLMs on five formal analysis capabilities, with results showing top model Claude-3.5 scores 48.7/100 and most models struggling on generation, transformation, and correction.
-
TheoremGraph: Bridging Formal and Informal Mathematics
TheoremGraph builds a unified statement-level dependency graph across informal arXiv math and formal Lean code via parsing, embeddings, and LLM validation, releasing the data and APIs for search and retrieval.
-
Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search
Fine-tuned 0.6B LLMs with beam search achieve 85% success on 60 test Shannon entropy inequalities (n=10-15), outperforming GPT-5.5 (1.7%) and Psitip (33.3%).
-
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
LeanMarathon uses four contract-scoped agents on an evolving blueprint coordinated by a two-stage orchestrator to formalize seven theorems from Erdős problems in Lean, proving 258 lemmas with no sorry across three runs.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
-
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
An RL-guided MCTS proof search for Tamarin finds more and shorter proofs than standard search across 16 protocol models.
-
Advancing Mathematics Research with AI-Driven Formal Proof Search
An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.
-
What are the Right Symmetries for Formal Theorem Proving?
Introduces rewriting categories to formalize proof equivariance and success invariance, shows LLM provers violate both, and demonstrates test-time aggregation recovers invariance and boosts performance.
-
CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
CAM-Bench is a new Lean 4 theorem-proving benchmark of 1,000 problems in computational and applied mathematics, built from textbook exercises using a dependency-recovery pipeline to reconstruct local context.
-
ABD: Default Exception Abduction in Finite First Order Worlds
ABD benchmark evaluates LLMs on producing parsimonious first-order exception formulas in three observation regimes using SMT verification, finding high validity but persistent parsimony and generalization gaps.
-
Massive Activations in Large Language Models
Massive activations are constant large values in LLMs that function as indispensable bias terms and concentrate attention probabilities on specific tokens.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
The signal-coverage matrix stratifies autoformalization outputs into true success, type-only, semantic-only, and both-fail cells, showing type-correctness gains are mostly type-stratum recovery with semantic errors largely unchanged.
-
OrthoReg: Orthogonal Regularization for Hybrid Symbolic-Neural Dynamical Systems
OrthoReg penalizes overlap between symbolic and neural components in hybrid dynamical models, improving symbolic recovery and out-of-distribution behavior under partial library mismatch.
-
VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
VERITAS improves zero-shot formal theorem proving to 40.6% on miniF2F and 7.3% on a new combinatorics benchmark by routing verifier signals into a two-phase Best-of-N then critic-guided MCTS protocol.
-
Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
A proxy-judge framework for autoformalization organizes checks into three structural scopes to produce a verdict vector that drives targeted refinement, with geometric contraction of the intrinsic gap under bounded judge noise.
-
Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification
EVA extracts continuous expected values from discrete token distributions in generative reward models via auxiliary MSE loss, instantiated as Leibniz for Lean 4 formal verification.
-
Automating Formal Verification with Agent-Guided Tree Search
Agent-directed tree search improves LLM performance on Lean formal verification tasks, with context-based orchestration solving more intermediate specs at lower token cost than baseline agents.
-
ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
ImProver 2 combines a data-efficient expert-iteration pipeline with a neurosymbolic scaffold to train a 7B model that outperforms larger models in Lean 4 proof optimization across structural metrics.
-
RMA: an Agentic System for Research-Level Mathematical Problems
RMA, a multi-agent system with structured memory and iterative feedback loops, solves 8 out of 10 research-level math problems on the new First Proof benchmark and outperforms GPT-5.2R and Aletheia according to expert evaluation.
-
OProver: A Unified Framework for Agentic Formal Theorem Proving
OProver-32B achieves top Pass@32 scores on MiniF2F, ProverBench, and PutnamBench by combining continued pretraining with iterative agentic proving, retrieval, SFT on repairs, and RL on unresolved cases using a 6.86M-proof dataset.
-
Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
Segment-level supervision extracts coherent proof segments to train policy models that achieve 61-66% success on miniF2F, outperforming step-level and whole-proof methods while also improving existing provers.
-
Measuring Representation Robustness in Large Language Models for Geometry
LLMs display accuracy gaps of up to 14 percentage points on the same geometry problems solely due to representation choice, with vector forms consistently weakest and a convert-then-solve prompt helping only high-capacity models.
-
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
A neuro-symbolic system using LLM-guided best-first search and Isabelle tools proves up to 77.6% of theorems on the seL4 benchmark, outperforming prior LLM methods and Sledgehammer.
-
VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
VERGE decomposes LLM outputs into atomic claims, autoformalizes them to first-order logic, verifies with SMT solvers and consensus, and refines via minimal correction subsets, yielding 18.7% average uplift on reasoning benchmarks.
-
Aristotle: IMO-level Automated Theorem Proving
Aristotle reaches gold-medal-equivalent performance on 2025 IMO problems via integrated Lean proof search, informal lemma formalization, and a dedicated geometry solver.
-
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
DeepSeekMath 7B reaches 51.7% on MATH via continued pretraining on curated web math data and Group Relative Policy Optimization.
-
Llemma: An Open Language Model For Mathematics
Continued pretraining of Code Llama on Proof-Pile-2 yields Llemma, an open math-specialized LLM that beats known open base models on MATH and supports tool use plus formal proving out of the box.
-
ToRA: A Tool-Integrated Reasoning Agent for Mathematical Problem Solving
ToRA trains language models on interactive tool-use trajectories with imitation learning and output shaping to integrate reasoning and external tools, yielding 13-19% gains on math datasets and new highs like 44.6% on MATH for a 7B model.
-
Solving math word problems with process- and outcome-based feedback
On GSM8K, outcome-based supervision achieves similar final-answer error rates to process-based with less labeling, but process-based or learned reward models are needed to reach 3.4% reasoning error among correct solutions.
-
Measuring Coding Challenge Competence With APPS
APPS benchmark shows models like GPT-Neo pass roughly 20% of test cases on introductory problems, indicating machine learning is beginning to learn basic coding.
-
Formalizing Scarf, Brouwer, and Nash in Lean
Lean 4 formalization of Scarf→Brouwer→Nash via Ivanov’s indexed-order Scarf theorem, grid instantiation, product embedding, and the Nash map, plus an 80-item BrouwerBench.
-
The Two-Hump Problem: Bridging the Difficulty Gap in Mathematical Reinforcement Learning
The authors identify a structural barrier ('two-hump' difficulty distribution) in RL for mathematical search problems like the Andrews-Curtis conjecture and propose data generation plus algorithmic enhancements to create solvable intermediate instances, releasing AC-19 and AC-1M datasets.
-
From Meta Idea to Advanced Mathematical Discovery -- Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms
Human-AI collaboration expanded a meta-idea on rational approximation into sign-embedding quantum algorithms for matrix problems, with humans retaining final judgment on routes and refinements.
-
(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
Trellis applies process semantics to guide generalist LLM agents through incremental refinement of proofs for reliable Lean autoformalization, shown via a Ramsey theory example.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
-
NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
NeuroNL2LTL presents a neurosymbolic system with verifier-in-the-loop RL training for NL-to-LTL translation, reporting 28% semantic equivalence and 86% satisfiability on 200k+ requirements across domains.
-
OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
OptProver transfers formal theorem proving from Olympiad math to optimization via continual training, achieving SOTA Pass@1 and Pass@32 on a new Lean 4 benchmark while retaining general performance.
-
Rethinking Wireless Communications through Formal Mathematical AI Reasoning
Proposes a three-layer framework using formal AI reasoning for verification, derivation, and discovery in wireless communications theory.
-
AI for Mathematics: Progress, Challenges, and Prospects
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
-
Step-Video-T2V Technical Report: The Practice, Challenges, and Future of Video Foundation Model
Step-Video-T2V describes a 30B-parameter text-to-video model with custom Video-VAE, 3D DiT, flow matching, and Video-DPO that claims state-of-the-art results on a new internal benchmark.
-
ReasonOps: A Unified Operational Paradigm for Trustworthy Verified LLM Reasoning
ReasonOps proposes treating LLM reasoning as a continuously monitored, verifiable operational process that unifies multiple verification techniques into a lifecycle to address inconsistencies and hallucinations.
-
Shaping Schema via Language Representation as the Next Frontier for LLM Intelligence Expanding
Advanced language representations shape LLMs' schemas to improve knowledge activation and problem-solving.
-
When control meets large language models: From words to dynamics
The paper proposes a bidirectional continuum between LLMs and control systems, covering LLM-assisted controller design, control-based LLM steering, and state-space modeling of LLMs.
-
Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoning
Position paper claims multimodal LLMs can significantly advance scientific reasoning and proposes a four-stage roadmap plus challenges and suggestions.