Tau Ceti 项目用 AI+Lean 形式化「全部基础数学」，人人可投算力参与
AlexKontorovich · x · 2026-11-03
Lean 官方转发介绍 Tau Ceti 项目：用 AI 大规模构建形式化数学库，由 Lean FRO 与 Mathlib Initiative 孵化。
- 工作流程：人类撰写 roadmap 规定目标数学内容，Lean 内核验证 AI 贡献的每条证明；再由「对抗性 AI 审稿人」检查定义与陈述是否符合 roadmap 意图、代码是否可供他人在其上构建。
- 目标：提供「全部基础数学」的可复用形式化，让研究者能借此直达研究前沿。项目位于 Mathlib 下游，尽量遵循 Mathlib 的设计决策，Mathlib 一旦形式化相关内容就切换过去。
- 参与方式：官方称人人可以「倒入算力」——安装 TauCetiWorker 后（需 Claude Code 或 ChatGPT Codex 账号），worker 会以你的 GitHub 账号审阅他人 PR 并按 roadmap 生成新的形式化 PR；roadmap 由人类架构师协调，任何人可提议和参与策展。
「编程与Agent」频道最新
- 150 名黑客齐聚 MIT 科学黑客松，用 Agent 系统攻科研问题 — ProfBuehlerMIT · 2026-11-03
- f1-graph-qa：自然语言查询 F1 历史的 text-to-Cypher Agent — JeremyCMorgan · 2026-11-03
- Figma PM 用 Claude Code 搭出 31 个 skill 的 PM OS，全司 60-70 名 PM 在用 — beeonaposy · 2026-11-03
- addTaskManager 推出 MCP 服务器，手机任务管理接入 AI — modelcontextprotocol · 2026-11-03
- News Sentiment Trends MCP：任意话题的新闻情绪趋势查询 — modelcontextprotocol · 2026-11-03
- LangChain Interrupt 大会第三届定档 2027 年 3 月，可容纳约 2000 人 — hwchase17 · 2026-11-03