**Tau Ceti：由人类规划、AI 实现的 Lean 数学库**

_AIs-welcome Lean library downstream of Mathlib_

> Tau Ceti 是 Mathlib 的下游项目，旨在构建一个完全由 AI 编写和审查的形式化数学库。人类负责制定路线图和审查标准，AI 负责代码实现与质量把控，致力于以最高质量形式化基础数学材料。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-07-25 20:32（北京时间）
- **原文**：[打开原文](https://github.com/TauCetiProject/TauCeti)