史上最大数学证明获计算机验证:有限单群分类 Lean 化完成
rickasaurus · x · 2026-10-28
Axiom 宣布完成有限单群分类定理(CFSG)的完整 Lean 形式化,号称人类历史上最大的数学证明:约 15000 页原始证明、500+ 篇论文、约 100 位数学家跨越数代的工作,被压缩为超过 4300 万行 Lean 代码,并在此过程中发现文献中约 100 处实质性修正。CFSG 被称为「对称性的元素周期表」,是 20 世纪数学的里程碑。配图为该形式化证明的全景依赖图,按里程碑、定理、定义、证书等节点类型分层展示。
所属事件:有限单群分类定理完成 Lean 形式化，史上最大证明获机器验证(21 条相关)→
「模型」频道最新
- 开发者用 EmbeddingGemma 2 搭实时嵌入端点：文本 20ms，全程只跑 MacBook CPU — generativist · 2026-10-28
- Google Gemma 官方汇总 EmbeddingGemma 2 社区项目：从 WebGPU 图搜到 Apple Silicon 加速 — GlennCameronjr · 2026-10-28
- DeepSeek 对话中自称「我是 ChatGPT」还提到 Claude，蒸馏争议再起 — ResonantFork · 2026-10-28
- LFM3-Audio 发布，开发者实现 100% 本地与台灯语音对话 — ngxson · 2026-10-28
- 同一开发者补刀:GPT-5.6 terra 若降价 80% 而非 20% 可能成爆款 — JoshPurtell · 2026-10-28
- 开发者质问 OpenAI:GPT-5.6 mini/nano 先涨价又只给 luna 降价,terra 为何不降 — JoshPurtell · 2026-10-28