Lean Pool: An AI-Maintained Archive of Formalized Mathematics
Vasily Ilin
cs.AI
2026-09-22
华盛顿大学用AI agent汇入、升级并压缩已完成的Lean形式化项目，现有211项、322万行；一次全库压缩删除45217行，干净编译缩短3.3%。
Lean 能机械检查证明，但 Mathlib 靠人审，体量近似线性增长，研究级数学常用的定义和定理经常不在库里。带 Lean 证明一起发布的长论证已经说明：形式化正在变成论文写出来就能核对的配套物。核对完还要能被后来者 import。源码躺在各自仓库里，Lean 和 Mathlib 一升级就编不过。
华盛顿大学的 Vasily Ilin 做了 Lean Pool：把已经完成的、有名字的已知结果形式化，收进同一个 Lean/Mathlib 环境，用 AI agent 负责发现、升级、压缩，人盯 merge。目标是形式化版的 arXiv，摩擦尽量低。
入库两条路。agent 去找 Apache-2.0 或 MIT 的完整形式化项目，升级 Lean 版本、过 CI 和 linter、过 LLM 审稿，再优化编译时间和内存；人也提交自己的项目。只收认真做完的、有名字的已知结果，允许人和 AI 混写。
准入很硬：不能有 sorry 或 admit；公理只许 Classical.choice、propext、Quot.sound；禁止 setoption 和绕过资源上限的手法；每项要有项目卡，写清作者、上游、证明出处和主要结果的非形式陈述。
日常工作是一组定时任务：搜新项目、看未合 PR、修 maintainer issue、压缩已有代码、在 Zulip 发公告。依赖升级工作流会探测新的 Lean/Mathlib，把编不过的项目分给修复 agent，再把补丁收成一轮审查。数学审稿服务看陈述是否忠实、是否重复、代码是否干净；维护者可以按报告改。
观察时点：211 个完成项目，7043 个 Lean 文件，3,228,485 行（含空行和注释），193,862 条声明，837 个登记的主要结果。证明出处 70 项人写、102 项 AI、39 项混合。GitHub 贡献者 18 人，社区合入 PR 63 个。Lean 版本升过 6 次。
最大的单项是有限时间 Navier–Stokes/Euler blowup，AI 写的，641,073 行。Gödel 不完备是人写的，55,430 行。
依赖升级很疼。4.32.0-rc1 升到 4.33.0-rc1，143 个项目里 100 个编译失败；4.34.0-rc1 升到稳定版 4.34.0，191 个里 97 个失败。中间也有轻的：4.33.0-rc2 到 4.34.0-rc1 只有 3/148 失败。稳定版迁移投了 97 个修复 job，95 个成功，剩下 2 个（图的基本群、不完备）靠后续集成补上，共改 639 个文件、5,951 行。
全库优化里，一次 compression 删 45,217 行，干净编译 16.11 分钟降到 15.59（快 3.3%）；elaboration 成本那次删 54,965 行，28.46 分钟到 26.82（快 5.8%）。贡献者 golfing 删了 12,515 行，编译反而慢 5.4%，内存略降。Navier–Stokes 抽可复用 API 让单项编译 879.67 秒变成 887.78 秒。
同一台 Azure 机器上，Lean Pool 干净编译 60.28 分钟、峰值内存 20.03 GiB；对齐版本的 Mathlib 是 37.44 分钟、7.35 GiB。LeanEval 的结构审计里，Lean Pool 是被后续解答匹配到最多的外部仓库。
LLM 审稿留下 188 次批准、71 次要求修改、37 次讨论。历史 API 估价 285 份报告合计 308.52 美元、中位 0.20 美元；后来的 Codex 等价估价 6 份合计 752.38 美元、中位 89.03 美元。同一 PR 重复审稿 69 对里只有 37 对结论一致。这套结构化审稿在观察时点前已被人手关掉。
autoformalization 的产出正在堆起来，缺的是能跟着 Mathlib 一起活的公共住所。Lean Pool 不把项目揉进统一 API（那是 Mathlib 和 Tau Ceti 的路），只保证独立项目能在同一环境里编过、能被搜到、能被后来者 import。对写证明的 agent 来说，这比再做一个更大的 Mathlib 更贴近现在的工作方式：项目是项目，引用关系另算。
对从业者，可直接当依赖用；对做形式化 agent 的人，这是一份带 CI、升级日志和失败率的运维记录，不是概念设计。
作者声明：人手写的部分只有一页，其余几乎全是 AI 生成。数字号称从保留的源码和执行记录算出来，并做了哈希校验，但论文主体的叙述质量要按「AI 起草、人负责」来读。
LLM 审稿没有独立标注对错，只记录了 merge 或关闭。同一 PR 重复审稿一致性 37/69，说不上稳。服务已经停，最近导入的项目不在这套覆盖里。自动修复之后仍要后续集成，稳定版迁移改了可测性、σ-有限性一类辅助假设，编译过关不等于每个声明类型升级前后等价。golfing 会让编译变慢。可复用接口有编译税。整库比 Mathlib 更重、更吃内存，规模继续涨时 agent 维护是否跟得上，这篇只给出到 Lean 4.34 的操作记录。