2026 年 6 月，Tau Ceti 还是一个新仓库。到 7 月 31 日的固定快照，它已经有 932 个 Lean 源文件、171,565 行代码和 1,336 个已合并 PR。在最忙的一天，100 个 PR 进入 main。
如果只看这些数字，Tau Ceti 很容易被概括成“AI 正在复制 Mathlib”。但我把它的五个组织仓库、Worker、review archive 和依赖更新链条全部拉到本地后，发现真正值得研究的并不是 AI 写 Lean 有多快，而是它怎样重组了一座数学库的生产关系：
人类写 roadmap 和 rubric，AI 写代码、修代码、审代码；Lean kernel 与 trusted CI 负责机械裁决；每一次 review 都成为公开数据。
这不是一个更大的 theorem-proving benchmark，而是一套正在运行的 formal-library operating system。
2026 年 7 月 30 日，Timothy Chow 在 MathOverflow 发了一个标题很直接的问题：Are we stuck with Lean?
截至本文抓取页面时，这个刚出现一天的问题已有 39 票、超过 1.6 万次浏览、6 个回答。它紧跟在 Lean 的 Collatz-themed soundness 事件之后：一份 AI 参与生成的 artifact 同时穿过了当时的 Lean kernel 与旧版 nanoda。于是一个工程事故很快被推到更大的问题上：
Are there any prospects for any organization to seriously support an alternative to Lean?
如果只按标题回答，讨论很容易变成两种口号：Lean 已经赢了，接受现实；或者 Lean 有过 soundness bug，应该换成 Metamath。六个回答和几十条评论真正说明的是：“被 Lean 锁定”不是一个 yes/no 问题，因为这里至少有六种不同的锁。
短期内，数学形式化确实在 Mathlib、工具链和共同体层面形成了很高的 switching cost；但这不等于 Lean 的 kernel、逻辑基础或今天的实现会永远不可替代。比“全部迁移”更现实的目标，是降低不可逆性：让重要证明能被独立 checker 复核、能跨系统重建，让替代生态得到长期工程投入。
MathOverflow 讨论仍在变化。本文中的票数、浏览量和回答数是 2026 年 7 月 31 日的快照；观点均按作者归属，不代表 MathOverflow、Lean 社区或本文的共同结论。