AI 推翻 87 年数学猜想，Lean 已完成形式化验证
rohanpaul_ai · x · 2026-07-22
AI 找到一个反例，推翻了一个已有 87 年 历史的猜想。这个问题最早由一位德国数学家在 1939 年 提出，核心是在讨论某类多项式映射：给定输出后，能否总是唯一恢复输入。
- 在 Anthropic 工作的 Levent Alpöge 证明了答案是否定的。
- 这条结果已经被 Lean 形式化验证系统检查通过。
- 原帖借此强调：AI 在数学中的优势正在快速逼近人类。
「漫话AGI」频道最新
- AI 实验室员工对“明年能做到什么”明显沉默了 — ChrisGPT · 2026-07-27
- AI 可能通过科研垃圾内容侵蚀科学体系 — rbhar90 · 2026-07-27
- 组织本身或许就是地球上的超智能 — eldonredwards · 2026-07-27
- AI 竞赛里的持久护城河可能只剩能源和信息 — GregKamradt · 2026-07-27
- 有人主张先造 AGI，再把它开源 — wordgrammer · 2026-07-27
- Jason Crawford 说 AI 不该只谈对齐，而该守法守伦理 — Afinetheorem · 2026-07-27