LeanCat

LeanCat是由清华大学等机构联合创建的范畴论形式化基准数据集，包含100个完全形式化的定理声明，涵盖基本范畴属性、伴随函子、极限与余极限等8个主题。该数据集通过专家筛选和LLM辅助流程构建，难度分为三个等级（简单20/中等42/困难38），旨在评估AI系统在抽象数学结构中的推理能力。数据源自《Category Theory in Context》等经典教材及前沿研究论文，采用Lean 4语言在mathlib库中实现，主要应用于形式化数学验证和定理自动证明领域，为解决现代数学中高阶抽象推理的自动化瓶颈提供测试平台。

LeanCat is a formal benchmark dataset for category theory jointly created by Tsinghua University and other institutions. It comprises 100 fully formalized theorem statements covering 8 topics including basic category properties, adjoint functors, limits and colimits, etc. Constructed via expert screening and LLM-aided workflows, the dataset is divided into three difficulty levels: 20 for simple, 42 for medium, and 38 for difficult, aiming to evaluate the reasoning capabilities of AI systems in abstract mathematical structures. The data is sourced from classic textbooks such as *Category Theory in Context* and cutting-edge research papers, and is implemented in the mathlib library using the Lean 4 programming language. It is primarily applied in the fields of formal mathematical verification and automated theorem proving, serving as a testbed for resolving the automation bottleneck of high-order abstract reasoning in modern mathematics.

原始信息汇总

LeanCat 数据集概述

数据集基本信息

• 数据集名称：LeanCat: A Benchmark Suite for Formal Category Theory in Lean 4
• 核心内容：一个包含 100 个陈述级问题 的基准测试套件，专注于 Lean 4 (mathlib) 中的形式化范畴论。
• 设计目标：旨在对形式化数学中依赖大量抽象和库基础的推理能力进行压力测试。

数据集结构与内容

• 主要领域：Part I 专注于 1-范畴论。
• 问题总数：100 个。
• 问题类别与数量分布：
  1. 基本范畴性质：问题 1-18。
  2. 伴随函子：问题 19–24, 26–29。
  3. 反射与余反射子范畴：问题 30-33。
  4. 具体范畴：问题 34-41。
  5. 极限与余极限：问题 42-73。
  6. 余完备化：问题 74-78。
  7. 阿贝尔范畴：问题 79-90。
  8. 单子：问题 24, 91-100。
• 难度分布：
  • 简单：20 个问题（难度评分 ≤6/10）。
  • 中等：42 个问题（难度评分 6-8.5/10）。
  • 高难度：38 个问题（难度评分 ≥8.5/10）。

技术规格与依赖

• 形式化语言：Lean 4。
• 数学库：mathlib。
• 所需 Lean 版本：4.19.0。
• 构建工具：Lake。

仓库文件结构

LeanCat/ ├── CAT_statement/ # 基准测试问题的形式化 Lean 4 陈述 ├── problems/ # 自然语言问题描述（Markdown 格式） ├── CAT_statement.lean # 包含所有陈述导入的主 Lean 4 文件 ├── lakefile.lean ├── lean-toolchain # 指定使用 Lean 4.19.0 ├── metadata.json # 问题元数据（难度、标签、引用） ├── lake-manifest.json └── LICENSE

相关资源

• 论文 arXiv 地址：https://arxiv.org/abs/2512.24796
• 引用格式： bibtex @article{xu2025leancat, title={LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)}, author={Xu, Rongge and Dai, Hui and Fu, Yiming and Jiang, Jiedong and Nie, Tianjiao and Wang, Hongwei and Wang, Junkai and Yang, Holiverse and Yang, Jiatong and Zhang, Zhi-Hao}, journal={arXiv preprint arXiv:2512.24796}, year={2025} }

搜集汇总

数据集介绍

构建方式

在范畴论这一高度抽象的数学领域中，LeanCat数据集的构建体现了严谨的学术流程。其构建始于专家团队从《Category Theory in Context》和《Abstract and Concrete Categories》等经典教材中精心筛选核心问题，旨在覆盖范畴论的基本属性、伴随函子、极限与余极限、单子等八大主题簇。随后，研究团队采用大语言模型辅助起草与人工验证相结合的三阶段工作流：首先利用多个先进模型生成Lean 4形式化语句草案，再由领域专家进行语义审核与修正；对于模型无法正确形式化的难题，则通过线下研讨会组织Lean专家进行人工编写。最终，所有形式化语句均经过独立评审员的完整一致性检查，确保其编译无误且与原始数学含义精确匹配，从而形成一个包含100个独立定理证明任务的标准化基准。

特点

LeanCat数据集的核心特征在于其专注于测试抽象推理与库介导的证明能力。与侧重于奥数技巧或本科竞赛题的传统定理证明基准不同，该数据集的问题设计强调在成熟的形式化数学库（mathlib）中进行高层级、结构化的接口级推理。其任务均为独立的语句级证明，不提供阶梯式提示，迫使求解器必须自主进行库检索、定义管理与抽象导航。数据集通过结合大语言模型尝试与人类专家评级的混合流程，为每个问题标注了易、中、高三个难度等级，其性能评估清晰揭示了当前模型在抽象层级提升时准确率的急剧下降，凸显了其在衡量长期规划与库知识整合方面的独特压力测试价值。

使用方法

LeanCat数据集的使用旨在系统评估自动定理证明系统在形式化范畴论中的能力。评估遵循标准化的pass@k协议：对于每个模型与问题对，在统一的提示词和工具设置下进行至多k次独立的证明尝试，只要有一次尝试生成的Lean代码能通过编译器验证即视为成功。评估环境严格一致，包含相同的Lean 4与mathlib库版本、上下文预算及验证时间限制。研究者可通过分析模型在不同难度等级（易/中/高）上的pass@1与pass@4成功率，定量衡量其处理抽象推理和库导航的稳健性。此外，数据集支持与LeanBridge等检索增强证明工具结合使用，通过检索-分析-生成-验证的循环，探索工具辅助工作流在提升证明鲁棒性方面的潜力。

背景与挑战

背景概述

在形式化定理证明领域，大型语言模型的快速发展催生了对于抽象推理与库中介推理能力评估的迫切需求。LeanCat数据集由清华大学丘成桐数学科学中心等机构的研究团队于2025年创建，旨在填补现有基准在范畴论形式化方面的空白。该数据集聚焦于范畴论这一现代数学的统一语言，通过100个在Lean 4中完全形式化的命题级任务，系统评估自动化证明器在成熟数学库中操作与组合高层抽象的能力。其核心研究问题在于检验人工智能是否能够驾驭研究级数学所依赖的接口级推理与结构性思维，从而推动形式化数学与人工智能证明技术的交叉前沿。

当前挑战

LeanCat数据集所应对的核心领域挑战在于，如何准确衡量自动化证明器在抽象、库依赖的数学推理中的真实能力，这超越了传统基于竞赛或教科书问题的基准。在构建过程中，研究团队面临多重具体挑战：首先，从经典范畴论教材与研究文献中筛选并形式化命题，需确保其覆盖核心接口并体现代表性证明模式；其次，部分高阶命题在现有数学库中缺乏直接引理，迫使人工形式化者先行开发中间结果，增加了数据构建的复杂度；最后，确立一套结合大模型评估与专家判定的难度标注流程，以客观反映问题在抽象导航与长程规划上的实际求解难度，这本身即是一项严谨的元评估挑战。

常用场景

经典使用场景

在形式化定理证明领域，LeanCat数据集为评估大型语言模型在抽象数学推理方面的能力提供了关键基准。该数据集聚焦于范畴论这一现代数学的统一语言，通过100个完全形式化的定理声明，系统测试模型在成熟数学库（如Lean的Mathlib）中进行结构性、接口级推理的效能。其经典使用场景在于作为压力测试工具，衡量自动化证明器能否在复杂的抽象框架内导航，并组合高阶定义与引理，而非仅仅解决孤立的计算性问题。

实际应用

在实际应用中，LeanCat数据集可作为持续跟踪人工智能与人类在形式化数学领域进展的可重用检查点。其任务设计紧密贴合数学库开发，成功解决方案可被合并至Mathlib等正式库中，形成从基准测试到库强化的反馈循环。此外，该数据集为改进工具增强工作流（如检索-生成-验证循环）提供了实验平台，例如通过LeanBridge集成Mathlib检索与编译器反馈，显著提升了在部分问题上的证明鲁棒性，展示了其在推动自动化证明工程实际部署中的价值。

衍生相关工作

LeanCat数据集的推出催生了一系列围绕抽象数学形式化的衍生工作。其设计理念与FATE等代数焦点基准形成互补，共同拓展了形式化推理的前沿。基于该数据集，研究者开发了如LeanBridge的检索增强证明框架，通过整合LeanExplore进行库检索与验证反馈，系统提升了证明生成的稳健性。未来计划扩展的系列（如针对幺半范畴、高阶范畴结构的基准）将进一步细化对抽象层次推理能力的诊断，激励跨系统比较与证明工程技术迁移，为领域发展奠定坚实基础。