TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
2026-06-08 • Artificial Intelligence
Artificial Intelligence
AI summaryⓘ
The authors created TheoremBench, a new benchmark to better test how well AI models can prove math theorems in a detailed and realistic way, beyond just short contest problems. They include both single-theorem tasks and groups of related smaller theorems to see how models handle complex proof steps. Their results show that giving models extra supporting statements helps, but current models still focus on easier parts and use long, inefficient proof methods. The authors also introduce new ways to measure how thoroughly and efficiently models prove the theorems. Overall, TheoremBench gives a clearer picture of AI's formal reasoning abilities in the Lean4 proof system.
theorem provingLean4benchmarkformal proofsubtheoremspremisesproof efficiencytacticsprover modelstoken efficiency
Authors
QuocViet Pham, Elvir Karimov, Andrey Galichin, Ivan Oseledets
Abstract
LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.