Tau Ceti 用 AI 与 Lean 形式化基础数学并开放算力参与

Tau Ceti 项目利用 AI 大规模构建基础数学的形式化库，由 Lean FRO 与 Mathlib Initiative 孵化。人类负责制定数学路线和协调策展，Lean 内核验证 AI 贡献的证明，对抗性 AI 审稿人则检查定义、目标符合度及代码可复用性。参与者安装 TauCetiWorker 后，可使用自己的 GitHub 账号审阅 PR，并依据 roadmap 生成新的形式化 PR。