Tau Ceti 发布：面向 Lean 的 AI 形式化数学库
wellecks · x · 2026-07-21
Tau Ceti 正式发布，这是一个面向 Lean 的 AI 形式化数学库，定位在 Mathlib 之下，强调可复用的形式化代码，而不是 Mathlib 那种“知识完备”的角色。
- 数学家负责提出 roadmap，AI 负责实现形式化内容，并在不断更新的 rubric 下互相审查。
- 项目欢迎贡献新的 roadmap、roadmap 审核和 AI 参与者，维护方也表示贡献者可以使用项目自带工具或自己的工作流。
- 该项目还与 Kim Morrison 和 Mathlib Initiative 共同孵化。
所属事件:Lean FRO推出Tau Ceti形式化数学库(3 条相关)→
「研究」频道最新
- Sakana AI 推出 Fugu-Cyber，称安全跑分只是开始 — SakanaAILabs · 2026-07-22
- Meta 用 SAM 3 和 DINOv3 将 3D 标注缩短到 15 分钟 — AIatMeta · 2026-07-22
- Project CETI 登上 Jeopardy!，题面玩起 SETI 式鲸类梗 — begusgasper · 2026-07-22
- 体细胞突变或将人类寿命上限锁定在 146 到 194 岁 — Anen-o-me · 2026-07-22
- 研究发现记忆压缩会让智能体丢掉安全规则，违规率高达 59% — gerardsans · 2026-07-22
- DriftWorld 宣称世界模型可跑 30+ FPS 且仅需 1–2 张 GPU — du_yilun · 2026-07-22