有限单群分类定理完成 Lean 形式化，4300万行代码揪出47篇论文96处错误
ChrSzegedy · x · 2026-11-03
- CFSG（有限单群分类定理）项目宣布完成第一代证明的完整 Lean 形式化：约 4310 万行 Lean 代码、205 万条声明、715 篇论文与书籍、100 个里程碑，覆盖这一定理由约百位数学家历时数十年写就、横跨数千页的经典证明。
- 形式化过程已在 47 篇经同行评审的顶级数学期刊论文（含《数学年刊》）中发现 96 处错误或缺口，凸显形式化验证的价值，尤其是在「vibeproving」时代。
- 项目还产出了新数学成果：论文《The Unbalanced Group Theorem》解释了已发表证明中的一处闭包断言反例，并基于 Solomon 1976 年极大 2-分量的理论给出替代论证。
所属事件:有限单群分类定理完成 Lean 形式化(2 条相关)→
「研究」频道最新
- AI 几分钟复现他 2021 年算了数月的羰基-烯烃复分解计算 — teortaxesTex · 2026-11-03
- 新论文：三个生产级 AI 均会钻评分器空子，还会顾及同伴分数 — jammastergirish · 2026-11-03
- 通用 LLM 加机械臂胜过专用机器人模型，bitter lesson 席卷机器人 — zakkohane · 2026-11-03
- 「这不算新研究」引争议：用 AlexNet 类比反驳被怼 — khademinori · 2026-11-03
- 预印本:1440 局博弈实验显示 LLM 智能体全部无视防敲竹杠合约 — shoumikgoswami · 2026-11-03
- Kimi K3.1 直接读懂网络原始权重，推理出被训练的是哪款游戏 — teortaxesTex · 2026-11-03