Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

Rongge Xu, Hui Dai, Yiming Fu, Jiedong Jiang, Tianjiao Nie, Hongwei Wang, Junkai Wang, Holiverse Yang, Jiatong Yang, Zhi-Hao Zhang

TL;DR

LeanCat addresses the gap between purely symbolic benchmarks and the abstraction-rich reasoning of modern mathematics by introducing a Lean 4, mathlib-based benchmark for 1-category theory. It assembles 100 statement-level problems across eight thematic clusters, curated through a three-stage process and annotated for difficulty, to probe library-grounded proving and long-horizon planning. Baseline evaluations across multiple models reveal a persistent abstraction and library-navigation gap, with the best pass@1 around $8.25\%$ and pass@4 around $12\%$, while a retrieval-augmented approach (LeanBridge) demonstrates selective gains. The work establishes LeanCat as a forward-looking stage for measuring AI and human progress in reliable, research-level formalization, and it lays out a roadmap toward richer categorical interfaces and cross-system benchmarking to strengthen formal libraries and proof engineering.

Abstract

Large language models (LLMs) have made rapid progress in formal theorem proving, yet current benchmarks under-measure the kind of abstraction and library-mediated reasoning that organizes modern mathematics. In parallel with FATE's emphasis on frontier algebra, we introduce LeanCat, a Lean benchmark for category-theoretic formalization -- a unifying language for mathematical structure and a core layer of modern proof engineering -- serving as a stress test of structural, interface-level reasoning. Part I: 1-Categories contains 100 fully formalized statement-level tasks, curated into topic families and three difficulty tiers via an LLM-assisted + human grading process. The best model solves 8.25% of tasks at pass@1 (32.50%/4.17%/0.00% by Easy/Medium/High) and 12.00% at pass@4 (50.00%/4.76%/0.00%). We also evaluate LeanBridge which use LeanExplore to search Mathlib, and observe consistent gains over single-model baselines. LeanCat is intended as a compact, reusable checkpoint for tracking both AI and human progress toward reliable, research-level formalization in Lean.

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

TL;DR

LeanCat addresses the gap between purely symbolic benchmarks and the abstraction-rich reasoning of modern mathematics by introducing a Lean 4, mathlib-based benchmark for 1-category theory. It assembles 100 statement-level problems across eight thematic clusters, curated through a three-stage process and annotated for difficulty, to probe library-grounded proving and long-horizon planning. Baseline evaluations across multiple models reveal a persistent abstraction and library-navigation gap, with the best pass@1 around and pass@4 around , while a retrieval-augmented approach (LeanBridge) demonstrates selective gains. The work establishes LeanCat as a forward-looking stage for measuring AI and human progress in reliable, research-level formalization, and it lays out a roadmap toward richer categorical interfaces and cross-system benchmarking to strengthen formal libraries and proof engineering.

Abstract

Large language models (LLMs) have made rapid progress in formal theorem proving, yet current benchmarks under-measure the kind of abstraction and library-mediated reasoning that organizes modern mathematics. In parallel with FATE's emphasis on frontier algebra, we introduce LeanCat, a Lean benchmark for category-theoretic formalization -- a unifying language for mathematical structure and a core layer of modern proof engineering -- serving as a stress test of structural, interface-level reasoning. Part I: 1-Categories contains 100 fully formalized statement-level tasks, curated into topic families and three difficulty tiers via an LLM-assisted + human grading process. The best model solves 8.25% of tasks at pass@1 (32.50%/4.17%/0.00% by Easy/Medium/High) and 12.00% at pass@4 (50.00%/4.76%/0.00%). We also evaluate LeanBridge which use LeanExplore to search Mathlib, and observe consistent gains over single-model baselines. LeanCat is intended as a compact, reusable checkpoint for tracking both AI and human progress toward reliable, research-level formalization in Lean.
Paper Structure (13 sections, 4 figures, 1 table)

This paper contains 13 sections, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. LeanCat Benchmark Design
  3. Benchmark Structure and Content
  4. Data Source
  5. Curation Workflow
  6. Statement-level tasks.
  7. Scope and difficulty.
  8. Formalization standards.
  9. Difficulty Annotation Pipeline
  10. Experiments and Results
  11. Evaluation Protocol
  12. Baseline Results and Analysis
  13. Discussion and Future Work

Figures (4)

  • Figure 1: Formal proof accuracy (pass@4) across LeanCat model baselines.
  • Figure 2: Intermediate natural-language (NL) vs. formal-language (FL) (pass@4) accuracy on LeanCat, highlighting the natural-to-formal gap.
  • Figure 3: Sunburst diagram showing the distribution of our LeanBridge problem sets by topic and difficulty. The inner ring groups problems into thematic sections (Basic, Adjunction, Reflective, Concrete, Limit, Cocompletion, Abelian, Monad), while the outer ring lists individual problems, labelled by difficulty: E = Easy, M = Medium, H = High.
  • Figure 4: We use LeanBridge to benchmark LeanCat across several LLMs. The table records, for each problem and model on natural-language statements, whether the model produced a correct statement or proof. A green cell indicates that the model produced a correct Lean proof of the intended statement. A blue cell indicates that the model produced a correct statement but without a correct proof. An olive cell indicates that the model's statement is not phrased in the same natural language as the original problem. A grey cell indicates that the output is not a complete Lean script (for example, it contains syntax or type errors).