# 数学家被 AI 反例打得措手不及

> 原标题：Human mathematicians are being outcounterexampled

- 来源：Hacker News 首页
- 发布时间：2026-07-20T19:03:37.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/45512
- 原文：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/

## 摘要

Kevin Buzzard 回顾了过去几周 AI 在数学形式化里连续找出反例的事。5 月 ChatGPT 用数论定理推翻了 Erdős 单位距离猜想；Logical Intelligence 在一周内把整篇论文自动转成了 Lean 代码。6 月 OpenAI 的 Boris Alexeev 用新模型 Sol 从公理出发完成了完整的形式化，生成了 120...

## 推荐理由

Kevin Buzzard 用第一人称给出了最近 AI 在形式化数学里连续找出反例的时间线，从 ChatGPT 推翻 Erdős 猜想到 OpenAI Sol 从公理出发完成形式化，细节扎实、叙事有张力，值得放在 featured。分数没拉满是因为这更像一篇个人观察和阶段性记录，正文没给出这些反例是否经过同行复核、模型在更广泛数学问题上的泛化表现也没展开。

## 锐评

Kevin Buzzard 这篇博客讲的是最近几周 AI 在数学证明里“找茬”的速度已经超过人类。5 月 ChatGPT 用数论定理推翻了 Erdős 单位距离猜想；Logical Intelligence 一周内把整篇论文自动转成了 Lean 代码。6 月 OpenAI 的 Boris Alexeev 用新模型 Sol 从公理出发完成了完整的形式化，生成了 120 万行 Lean 代码，其中包含全局类域论这种硬骨头——而人类维护的数学库 mathlib 花了九年才攒了 230 万行。7 月 Logos Research 的工具又在一个 LLM 生成的文档里揪出了一个关于有限平坦群概形的错误断言，人类作者自己都没发现。

Buzzard 的结论是“大规模 AI 生成的数学发展不可避免”。这个判断有数据支撑：120 万行代码三周跑完，对比人类九年的积累，速度差了两个数量级。但要注意，他明确说 AI 生成的代码不可信，得在沙箱里跑，因为 Lean 是编程语言，恶意代码能执行任意命令。这点先别太激动——形式化验证只是把数学陈述翻译成机器可检查的语言，不等于证明本身没有逻辑漏洞。

正文没披露的是：这些反例是否经过了独立的人类数学家复查？Sol 生成的 120 万行代码里有多少是冗余或垃圾？Buzzard 自己说代码“有时很糟糕”。另外，全局类域论的形式化到底覆盖了原论文 100 多页证明的多少比例，也没说清楚。