Trellis 自主运行 6 周形式化强完美图定理：54 万行 Lean 创纪录
littmath · x · 2026-09-03
普林斯顿教授 Wes Pegden 透露，AI 系统 Trellis 已完成对 强完美图定理（Strong Perfect Graph Theorem）的形式化——该定理由 Chudnovsky、Robertson、Seymour、Thomas 于 2006 年发表在《Annals of Mathematics》，长达 178 页，是图论里程碑。
关键事实：
- Trellis 自主运行 6 周完成形式化
- 产出证明达 54 万行代码，是迄今最大的 Lean 自动形式化成果
- 原论文与 Lean 证明的查看器、git 仓库均已公开
这展示了 AI 在大规模数学形式化上的新高度。
「研究」频道最新
- 技术圈质疑 Astra 循环架构:最可能只是每层跑两遍的调度 — mike64_t · 2026-09-03
- 研究者入选 Cosmos 计划，三个月攻关 LLM 思维忠实性 — hunarbatra · 2026-09-03
- Video Delta Net 让开源视频生成提速 75–90 倍，14 秒视频 11 秒生成 — xiuyu_l · 2026-09-03
- CoreAuto 发布神经网络架构自动发现新博客文章 — _arohan_ · 2026-09-03
- 研究者称其任务的强化学习「可能已被攻克」 — andrew_n_carr · 2026-09-03
- Pearl 回应 Harrell：RCT 新语言应检验其表达力边界而非强行推广 — yudapearl · 2026-09-03