AI4Math ChronicleAI4Math 大事记

Lean Pool 发布面向大规模形式化数学的 AI 维护档案库

该档案库有意采用不同于 Mathlib 的定位：它接收可能不适合 Mathlib 高度整合式库结构 的独立完整形式化项目，同时施加自动化维护与质量检查。公开仓库说明，目前项目导入 仍由人类选择，而 AI 系统实质参与审查、维护与优化。由于库规模持续变化，本 Event 不把某一时点的项目数或代码行数作为冻结的历史主张。

发生了什么？

Lean Pool 将自身定位为由 AI Agent 扩展、维护和优化的形式化数学仓库。项目接收已完成 的 Lean 开发，并要求通过全库构建、linter、风格和证明完整性门禁；确定性检查之外 还加入 LLM 审查，并持续把已收录项目迁移到新的 Lean 与 Mathlib 版本。其独立 challenge 工作流使用 Comparator 对照题目与解答陈述，并通过 Lean kernel 重放证明。

为什么重要？

随着 AI 生成和 AI 辅助的 Lean 项目增多，保存与维护开始成为不同于“证明单个定理” 的新瓶颈。Lean Pool 在高度精选的一体化数学库与松散独立仓库之间提供 AI 辅助档案层， 把版本维护、检索、质量门禁与 challenge 验证都纳入 AI4Math 基础设施问题。

重要性说明：Lean Pool 构成 AI 维护形式数学基础设施方向的领域级里程碑：它把大量独立 Lean 开发组织为持续维护的档案库，并配套确定性质量门禁、LLM 辅助准入审查、文档、 语义检索以及由 kernel 检查的 challenge 工作流。其历史意义在于展示 AI Agent 如何参与大规模形式化数学维护，而不是声称库内每个项目都由 AI 发现或编写。

历史脉络

更早进展
后续进展

—

相关里程碑

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
论文已发布
证据等级
E3 · 可检查工件
AI 角色
AI 实质性支持
形式保障
有形式化工件

如何理解这些标签？ →

贡献与验证

数学新颖性
工具性进展
接口
形式化
AI 贡献
AI Agent 实质参与仓库扩展、维护、优化与准入审查。仓库同时明确说明，目前项目仍由 人类选择并加入，而且其中许多形式化本身由人类编写，因此不能把整个档案库描述为 完全由 AI 创作的数学。
人类贡献
人类维护者建立档案库、选择候选项目、制定审查与质量政策、维护治理并可参与集成工作； 项目由 Vasily Ilin 与 Justin Asher 在 UW Lean Hackathon 期间创建。
验证状态
论文已发布 · E3 · 可检查工件 · 有形式化工件
最后审阅
2026-09-27

技术细节

系统
lean-pool, lean, gpt-6-astra, comparator
机构
—
数学问题
—
方法
ai-assisted-maintenance, formal-mathematics-archiving, llm-review, semantic-search, proof-integrity-checking

全部来源与工件

验证历史

  • 2026-09-21 · 论文已发布 · E3 · 可检查工件

    arXiv 记录与公开仓库确认了该档案库所述 AI 维护运作模式，并公开其 CI、审查和 challenge 验证机制。Reservoir 独立索引该 Lean package，并报告仓库版本的构建 结果。这些证据佐证基础设施的存在与运行，但并不认证持续变化的档案中每个项目 的数学语义或新颖性。

更正

当前没有记录的更正。