Trellis 在几乎无人类数学 steering 下完成 Strong Perfect Graph Theorem 与完整 Berge decomposition theorem 的 53 万+ 行 Lean 形式化

Wesley Pegden 宣布 Trellis 完成 Strong Perfect Graph Theorem 及其完整 Berge-graph decomposition theorem 的端到端 Lean 形式化。CMU 项目页记录：该 run 从 7 月 17 日持续到 9 月 1 日，约 1,460 个 supervisor cycles，最终接近 1,500 个 nodes、约 1,100 个 theorem-like statements、390 个 definitions、约 530,000 行 Lean。除 source manuscripts 与中途对 statement shapes 的人工确认外，没有提供数学内容、proof steps 或 Lean hints；所有 obligations 都在 isolated checker 中构建，无 sorry，且只使用标准公理。