# Dan Abramov 花一个月用 Claude 搞出了一个 50 年前 Conway 猜想的 Lean 证明

> 原标题：I Vibed a Proof of Conway's Conjecture

- 来源：Hacker News 首页
- 发布时间：2026-09-18T14:36:10.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/57361
- 原文：https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/

## 摘要

Dan Abramov 用了一个月的业余时间，让 Claude 在超现实数领域挑了个问题，最终给出了 Conway 1976 年提出的“全整整数细化猜想”的 Lean 形式化证明。这个证明已经通过了 Palomar 注册中心的机械检查，但还没有数学家独立验证过。他让模型自己选领域和题目，最后因为今年是 Conway《论数与游戏》出版 50 周年，选了这...

## 推荐理由

Dan Abramov 的第一人称实验 + 50 年未解猜想 + Lean 机械验证通过，三个点都踩中了。但我会先打个折：目前只有机器检查通过，没有数学家独立审阅，所以数学上的分量还没坐实。82 分给的是这件事的传播力和实验示范性，不是给证明本身的数学价值。

## 锐评

这条新闻有意思的地方在于，Dan Abramov 自己承认是“数学小白”，他让 Claude 自己选领域、自己挑题目，最后在超现实数这个冷门但漂亮的领域里，把 Conway 1976 年提出的“全整整数细化猜想”做成了 Lean 形式化证明。证明已经通过了 Palomar 注册中心的机械检查，这点是硬的，但正文也明确说“没有数学家独立验证过”，所以目前只能算机器说它对，人还没点头。

我会先打个折：机械检查通过不等于证明在数学上有意义，它只保证逻辑链条没断，不保证起点和定义没跑偏。另外，正文没披露具体花了多少 token，只说“一船”，成本完全是个黑箱。

还缺两样东西：一是数学家对证明本身的人肉审查，二是这个证明到底有没有带来新的数学洞察，还是只是把已知路径用 Lean 重走了一遍。如果只是后者，那更像一次极限编程实验，而不是数学突破。