AI 推翻 87 年数学猜想，Lean 已完成形式化验证
rohanpaul_ai · x · 2026-07-22
AI 找到一个反例，推翻了一个已有 87 年 历史的猜想。这个问题最早由一位德国数学家在 1939 年 提出，核心是在讨论某类多项式映射：给定输出后，能否总是唯一恢复输入。
- 在 Anthropic 工作的 Levent Alpöge 证明了答案是否定的。
- 这条结果已经被 Lean 形式化验证系统检查通过。
- 原帖借此强调：AI 在数学中的优势正在快速逼近人类。
「漫话AGI」频道最新
- 「AGI 已来」vs 现实：AI 实验室做的桌面应用依然又糙又卡 — MilesCranmer · 2026-09-11
- 前 OpenAI/Anthropic 研究员辞职,批两巨头正赌命冲向自我改进超智 — davidmanheim · 2026-09-11
- Anthropic 风险表态遭误引，2030 年毁灭概率争议再起 — davidmanheim · 2026-09-11
- 经济学家拆解 Anthropic 增长模型:能写出 15% GDP 增长,不代表会发生 — sebkrier · 2026-09-11
- Cohere Labs 推出交互工具:测 178 种职业哪些任务会被 AI 自动化 — Cohere_Labs · 2026-09-11
- AI 安全人士上 SkyNews 担忧不平等、滥用与社会激励结构 — schwarzjn_ · 2026-09-11