TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

Abstract

Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitional framework. However, frontier mathematics is often exploratory and prototype-heavy, relying on bespoke constructions that deviate from standard libraries. In this work, we evaluate the robustness of current ATP systems when applied to a novel definitional framework, specifically examining the performance gap between standard library problems and bespoke mathematical constructions. We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I, which formalizes analysis by constructing core mathematical concepts from scratch, without relying on standard Mathlib definitions, as well as by mixing from-scratch and MathLib constructions. For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem. To isolate the effect of definitional frameworks, we additionally translate every problem into a mathematically equivalent Mathlib formulation, yielding paired TaoBench-Mathlib statements for direct comparison. While state-of-the-art ATP models perform capably within the MathLib framework, performance drops by an average of roughly 26% on the definitionally equivalent Tao formulation. This indicates that the main bottleneck is limited generalization across definitional frameworks rather than task difficulty. TaoBench thus highlights a gap between benchmark performance and applicability, and provides a concrete foundation for developing and testing provers better aligned with research mathematics.

Figures (11)

• Figure 1: Tao's Analysis I constructs several mathematical structures in LEAN from scratch, often using formulations that diverge significantly from their equivalents in MathLib. TaoBench provides mathematically equivalent MathLib counterparts, and reveals a substantial degradation in model performance when navigating Tao’s specific definitional framework.
• Figure 2: Agentic framework for automatically extracting a compilable, self-contained local environment from a formalized textbook. The construction of references and dependencies for each exercise is performed using the JiXia tool. An agentic harness, equipped with a file-lookup tool and a Lean verifier, then iteratively builds a compilable, self-contained local environment.
• Figure 3: Translation pipeline for converting exercises from Tao's definitional framework to MathLib's. The rewriting and equivalence checking stages ensure the compilability and mathematical equivalence of TaoBenchMathLib, followed by expert verification for additional assurance.
• Figure 4: Model Performance vs. Definitions in Context. Performance on TaoBench and TaoBenchMathLib as a function of the number of in-context definitions. The performance delta is defined as performance (TaoBench) - performance (TaoBenchMathLib). DS, GD, and KM indicate DeepSeek-Prover-V2, Goedel-Prover-V2, and Kimina-Prover, respectively.
• Figure 5: Case studies: Nat.backwards_induction and Convergesto.squeeze. The textbook context for TaoBench is omitted due to space limitations. The full statements of the two exercises are shown in Figures \ref{['fig:case_study_full_1']} and \ref{['fig:case_study_full_2']}.