Lean Pool：由 AI 代理维护的形式化数学档案库
核心概要
Lean Pool 是一个由 AI 代理生长、维护与优化的形式化数学仓库，论文报告其截至 2026 年 9 月 21 日已汇集 211 个已完成项目、3,228,485 行 Lean 代码、18 位提交贡献者，并通过代理辅助的依赖升级、证明压缩与数学评审来维持这些独立开发的形式化成果在 Lean/Mathlib 演进中持续可用。
深度剖析
提出并运行一个“活的”形式化数学档案库：把独立开发、来源各异的已完成形式化项目汇集到统一的 Lean/Mathlib 环境中，并保留归属与项目组织。 与 Mathlib 这类由人类严格评审、线性增长的集成式数学库不同，Lean Pool 以“汇集 + 代理维护”的方式接纳人类、AI 与混合来源的项目，准入要求包括无 sorry/admit、不引入 Classical.choice、propext、Quot.sound 之外的公理、Apache-2.0 或 MIT 许可、以及标明作者、上游来源、证明来源与主要结果的 project card。 论文给出档案普查数据：211 个已完成项目、7,043 个 Lean 源文件、3,228,485 行物理源码、193,862 条声明命令、837 个登记的主要结果，人类/AI/混合项目分别为 70/102/39，18 位提交贡献者、17 位有合并 PR 的贡献者、63 个社区 PR 被合并。
代理辅助的依赖升级可以在 Lean/Mathlib 版本变化后恢复档案库的兼容性。 论文把“形式化成果的可复用性”从保存源码推进到持续维护：依赖更新工作流检测新版本、构建档案库、把失败项目分配给修复代理，再统一检查修复结果。 表 2 记录六次历史升级中受影响项目数与编译器失败数，例如 4.30.0-rc2 到 4.31.0-rc1 有 59 个项目在探测中、44 个编译失败；4.34.0-rc1 到 4.34.0 有 191 个项目、97 个失败。附录 D 记录稳定版迁移：191 个探测项目、97 个编译失败、97 个修复任务中 95 个成功、2 个失败，最终接受 198 个项目、改动 639 个文件、行变动 5,951。
共享档案库使跨项目的证明压缩与编译优化成为可能，并给出可测量的构建资源变化。 论文不只报告“证明变短”，还报告整库构建时间与峰值内存的前后对比，以及项目级编译秒数的变化。 表 3 列出被接受的改动，例如 187 号“库级压缩”删除 45,217 行、构建时间从 16.11 分钟降到 15.59 分钟、峰值内存从 26.1 GiB 变为 26.9 GiB；339 号“elaboration 成本削减”删除 54,965 行、构建时间从 28.46 分钟降到 26.82 分钟。表 4 给出项目级结果，例如量子并行重复从 141.85 秒降到 86.08 秒。附录 A.2 报告干净构建对比：Lean Pool 3.23 MLOC、60.28 分钟、20.03 GiB，Mathlib（匹配版本）2.33 MLOC、37.44 分钟、7.35 GiB。
把“陈述是否忠实于所宣称的数学贡献”纳入准入流程，并配套可检索的阐释站点与依赖图。 Lean 内核只保证证明正确，论文进一步用数学评审服务检查忠实性、新颖性、重要性、来源与代码质量，并用 exposition 站点把项目卡片、非形式说明、Lean 陈述与依赖图连接起来。 评审服务记录 285 份历史 API 估算报告、总计 308.52 美元、中位数 0.20 美元；同一 PR 的 69 对重复评审中 37 对给出相同结论。阐释覆盖 203 个项目、173,362 条源声明、124,412 条定理与引理、1,389,967 条依赖链接、87,408 条被多个声明使用的声明。附录 G.1 记录 Kurosh、Feige、Poincaré 等后续开发对档案库结果的复用。
启示与展望
这项工作面向的是已完成、命名已知结果的形式化项目，要求无 sorry/admit、公理受限、许可为 Apache-2.0 或 MIT，并需要 project card 标明作者、上游来源、证明来源与主要结果；开放挑战被单独放在 challenge board，不进入已完成集合。它使人类贡献者、AI 代理与后续研究者能够在统一的 Lean/Mathlib 环境中提交、检索、检查与复用形式化成果，并让依赖升级与优化成为可重复的日常流程。论文把 Lean Pool 定位为形式化数学的“活的档案库”，其目标是让形式化成果在 Lean 与 Mathlib 演进时仍保持可用，而不是替代非形式数学文献本身。
论文明确说明档案库与其自动化仓库持续变化，观测有明确时间点（如源码普查为 2026 年 9 月 21 日 06:07 UTC），因此表中数字是特定修订下的快照。评审服务在观测前已被手动停用，保留报告描述的是过去的执行，不构成对最新导入项目的持续覆盖；价格是保留报告上的估算而非账单，被覆盖或未记录的执 行无法从保留评论中恢复。附录 D 指出成功构建只确立接受陈述的兼容性，并不确立升级前后每条声明类型的等价性。此外，论文的人类撰写部分仅一页，其余几乎全部由 AI 生成，读者若需要更细的证明细节，应结合附录、源修订号与公开 PR 记录自行核对。