Claude 在 Lean 4 中完成三元哥德巴赫猜想的完整形式化
Singularitarian · x · 2026-11-11
Claude 完成了三元哥德巴赫猜想在 Lean 4 与 Mathlib 中的形式化证明。该猜想指每个大于 5 的奇数都可表示为三个素数之和，其证明基于 Harald Helfgott 2013 年宣布、此后多次更新的成果——由于原始证明中大量冗长计算难以核对，曾有专家质疑其正确性。
根据项目 README：
- 证明已完整：无任何 sorry，主定理仅依赖 Lean 标准三条公理；
- 两个已发表的数值验证结果作为显式假设引入：Platt 的 GRH 验证（q=1 时 RH 验证到 10^8）与二元哥德巴赫验证到 4×10^18。
这是 AI 驱动数学形式化的标志性成果，也间接回应了学界对 Helfgott 证明可验证性的担忧。
「漫话AGI」频道最新
- Reddit 网友：人均 GDP 达 20 万美元才是「后劳动时代」的门槛 — deferare · 2026-11-11
- 研究者担忧：若渐进式失权发生，谁来「拥有」科学进步 — najoungkim · 2026-11-11
- 陶哲轩：AI 缺少自己的香农信息论，没人知道规模化的上限 — burny_tech · 2026-11-11
- 同一批人既喊「与中国的AI竞赛不能减速」，又要求放松GPU出口管制 — austinc3301 · 2026-11-11
- Turing Post 社论：AI 能力过剩正让高效人群陷入倦怠焦虑 — TheTuringPost · 2026-11-11
- Redwood 争论:AI 安全技术工作即使在 2027 起飞情形下仍有价值 — austinc3301 · 2026-11-11