林岚｜OC 开发者生态编辑

据数学家 Kevin Buzzard 在 Xena Project 的观察，近期多项 AI 数学成果具有共同特征：人类长期相信某个命题可能成立，模型却通过大规模探索找到一个足以推翻它的反例。

一句话结论： 找到反例并不比证明“低级”，因为推翻一个全称命题只需要一个可靠例子；AI 的耐心、搜索广度和程序验证，恰好适合在人类直觉不愿探索的区域寻找它。

Erdős 的平面单位距离猜想就是代表案例。问题研究平面上若干点之间能有多少对距离恰好为一。人类长期围绕规则网格建立直觉，OpenAI 内部模型却找到高度不规则的构造，突破预期上界。数学家随后简化并人工核验，相关说明公开在 arXiv。

这不是“模型胡乱试数字”。一个有价值的反例必须满足全部定义，规模足够，并能被程序或形式系统复现。Lean 等证明助手的作用，是检查每一步是否遵守形式规则；它能排除计算和逻辑漏洞，却不能保证人类最初把问题翻译成 Lean 时没有写错。

AI 的优势也不意味着数学家下线。模型擅长扫过大量不美观方案，人类仍要判断问题是否重要、解释构造为何有效、把一次反例变成可理解的新理论。搜索得到答案和形成数学知识，是两个阶段。

关键事实

• OpenAI 模型给出 Erdős 单位距离猜想的反例，并经数学家核验整理。
• 推翻全称猜想只需一个有效反例，适合计算搜索与形式验证。
• Lean 验证形式推理，不会自动检查问题陈述是否忠实。

OC 判断

AI 数学的突破口未必是模仿天才写优雅证明，而是先成为一个不知疲倦、没有审美偏见的反例猎手。它会迫使数学家更早问一句：我们到底证明不了，还是命题本来就是错的？

为什么重要

• 对开发者： 搜索、程序执行和形式验证的组合比单次聊天更关键。
• 对研究机构： 应保存可复现构造和人工解释，而非只发布模型结论。
• 对读者： “AI 推翻猜想”不等于解决了该领域的全部问题。

参考来源

• Xena Project 原文
• OpenAI：模型推翻单位距离猜想
• arXiv：Remarks on the disproof