AI4Math ChronicleAI4Math 大事记

Mathlib3 建立面向协作式形式数学的共享 Lean 数学库

Mathlib 将社群编写的 Lean 定义、定理、证明与 tactics 组织为共享数学库，逐步覆盖代数、分析、拓扑、数论等领域；统一 API 与协作审查实践使形式化成果能够相互复用，而非停留在彼此隔离的项目中。

发生了什么？

保留至今的 leanprover-community/mathlib3 GitHub 仓库创建于 2017 年 7 月 21 日，因此本 Event 以该精确 artifact 时间作为 canonical 锚点。后来由 mathlib 社群发表的论文将该项目描述为在 Lean 中构建统一形式数学库的社区协作工程，并系统说明其数学结构、自动化与组织架构。

为什么重要？

现代学习式定理证明不仅需要证明检查器，也需要大规模形式陈述、证明状态与依赖关系语料。Mathlib 正是 Lean 生态中的这一基础层，后来直接支撑 LeanDojo 等环境、数据集以及大量基于 LLM 的形式数学系统。

重要性说明：Mathlib 把 Lean 从证明助手平台进一步发展为持续增长、可复用的共享形式数学语料库；其规模、协作开发模式以及机器可读的定理与证明数据，后来使其成为基于 Lean 的 AI 定理证明和基准构建的核心基础设施。

历史脉络

更早进展
后续进展
相关里程碑

—

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
尚属声明
证据等级
E3 · 可检查工件
AI 角色
仅计算支持
形式保障
有形式化工件

如何理解这些标签？ →

贡献与验证

数学新颖性
工具性进展
接口
形式化, 符号
AI 贡献
数学库内容主要由人类编写与审查，Lean 负责机械检查；本 Event 记录的是机器可读证明基础设施的形成，而非自主 AI 数学发现。
人类贡献
Lean 数学社群以协作方式在共享仓库中开发、审查并维护可复用的形式定义、定理、证明与自动化工具。
验证状态
尚属声明 · E3 · 可检查工件 · 有形式化工件
最后审阅
2026-09-27

技术细节

系统
lean, mathlib3
机构
leanprover-community
数学问题
formal-mathematical-knowledge
方法
mathematical-library, collaborative-formalization, proof-checking, interactive-theorem-proving

全部来源与工件

验证历史

  • 2017-07-21 · 尚属声明 · E3 · 可检查工件

    保留的公开仓库提供精确 GitHub 创建时间戳以及可直接检查的形式化 artifact；后来的 mathlib 论文记录了该数学库的社区协作架构与覆盖范围。

更正

当前没有记录的更正。