AI攻克Erdős猜想：Claude完成Lean 4形式化证明
ctjlewis · x · 2026-08-02
一个名为 EvolvingPrograms 的 GitHub 项目展示了 AI 在前沿数学领域的突破。该项目利用 Anthropic 的 Claude Fable 5 和 Claude Opus 5 模型，在 Lean 4 中完成了对 Erdős–Simonovits 退化猜想（Erdős 问题 #146）的形式化证明。
- 核心结论：该形式化过程证明了原猜想并非成立，而是“在所有层级上均失效”，并给出了在吉布斯权重为 $e$ 时的精确渐近律。
- 技术细节：整个证明过程完全基于 Lean 4 与 mathlib，且标注为“zero human commits”（零人工提交），意味着从构思到代码实现均由 AI 主导完成。
这一成果不仅展示了当代大模型在复杂逻辑推理和定理证明上的强大能力，也为 AI 辅助数学研究提供了一个极具说服力的标杆案例。
所属事件:Claude结合Lean 4成功证伪Erdős数学猜想(4 条相关)→
「编程与Agent」频道最新
- 开发者用3台DGX Spark组本地集群跑GLM-5.3-Flash,配代理均衡日生175万token — Teknium · 2026-10-16
- 开发者分享给电脑上的 Agent 划权限:能读能写,发删买一律先问人 — No_Fan5310 · 2026-10-16
- 开发者用GPT写出unifi-simulator,让MikroTik交换机伪装进UniFi网络拓扑 — Pytlicek · 2026-10-16
- 斯坦福 45 分钟课拆解 Grok Bot:always-on agent 的 harness 工程 — Hesamation · 2026-10-16
- Opus 5.5 + Three.js 打造水波鱼群樱花互动场景，美到刷屏 — nikola_mr64990 · 2026-10-16
- 用 Grok 搭建线性回归交易系统，125 天在 Polymarket 赚 50 万美元 — Roger_M_Taylor · 2026-10-16