Tau Ceti：AI编写的形式化数学库，与Mathlib互补

Tau Ceti 是一个由人工智能驱动的形式化数学库，由 Lean FRO 和 Mathlib Initiative 联合孵化，并与学术界和工业界合作。该项目的一个核心特点是，人类数学家负责制定路线图，而 AI 系统则根据这些路线图编写代码。所有贡献都通过 AI 驱动的审查流程，审查规则由人类编写并公开在 TauCetiReview 仓库中。Tau Ceti 与 Mathlib 的关系是互补的：它建立在 Mathlib 的基础上，但更注重快速构建可重用的数学库，而非精细的整理和消化。项目的目标是通过大规模的形式化工作，为前沿数学研究提供基础。

审查过程是敌对的，旨在发现错误或空洞的陈述，确保质量。AI 根据固定的开源规则进行审查，当 PR 打开时，先运行 CI（包括完整的 Mathlib 代码检查），然后根据规则给出“阻止”、“请求更改”或“批准”的判决。目前审查基础设施已搭建但尚未自动触发，可以通过命令行运行。此外，项目还引入了“元审查”系统，使用人类和 AI 评委对审查进行 A/B 测试，以量化评估审查质量。

Tau Ceti 依赖于 Mathlib 的主分支，并始终遵循 Mathlib 的设计决策。AI 被鼓励提交 PR 来更新 Mathlib 的依赖并修复相关问题。项目不会将材料向上游推送到 Mathlib，但 Mathlib 贡献者欢迎采用、整理和修改 Tau Ceti 的材料。所有代码采用 Apache 许可证。

该项目明确不旨在像 Mathlib 那样进行精细的策展和整理，而是专注于构建一个可重用、大规模的开放库。Tau Ceti 的哲学是，数学的产物是清晰和理解，而非仅仅定理本身。项目希望通过在 Tau Ceti 上构建下游形式化来逐步建立对 AI 编写定义的信任。信任不是通过初步审查实现的，而是通过将定义集成到更深的数学网络中，并在其之上证明更多定理来建立的。

在协作方面，Tau Ceti 使用“意图注册”机制，允许贡献者声明他们正在积极工作的路线图部分，从而避免重复劳动。该机制已内部使用，并计划扩展到公共项目意图注册中心，未来可能实现联邦系统。项目强调快速发展，为前沿研究提供基础，同时不干扰这些研究。Tau Ceti 是一个社区资源，欢迎所有人的参与。