近日，ChatGPT推翻了厄多斯单位距离猜想，但该反例尚未在Lean中形式化验证。这引发了对数学证明可信度的讨论，凸显了交互式定理证明器在未来数学中的重要性。

好的，这是根据您的要求，对原文主要内容的中文重述，保留了关键细节，并删减了与主题无关的冗余信息。

标题：人类数学家正在被“反例”超越

过去几周，数学反例领域发生了许多引人注目的事件。本文主要从我的视角，回顾形式化验证、AI工具，特别是反例方面的新进展。

单位距离猜想被推翻

两个月前（2026年5月20日），ChatGPT推翻了离散几何中的埃尔德什单位距离猜想。虽然已是旧闻，但值得一提。OpenAI的公告附有几位我认识且信任的数学家的证词，他们表示已提前审阅并相信该论证。该证明的核心是利用了1960年代Golod和Shafarevich的一个深刻数论定理来构造反例。

我首先关心的是这个反例是否已在Lean中形式化，答案是否定的。但不到一周，菲尔兹奖得主Mike Freedman告诉我，他所在的Logical Intelligence公司已将ChatGPT生成的论文自动形式化为Lean代码。我和博士后Thomas Browning检查后发现，他们确实形式化了该数论定理蕴含埃尔德什反例的论断。这标志着LLM生成的数学成果被实时形式化。

然而，这里有个难题：那个数论定理的证明长达100多页，涉及庞大的全局类域论，目前难以压缩。2025年我曾与Richard Hill举办过类域论形式化的暑期学校，一年后我们才基本完成局部情形，全局情形在当时看来仍是幻想。

一个月后（6月26日），Boris Alexeev宣布，他引导ChatGPT（使用新模型Sol）完成了埃尔德什反例的完整形式化，不依赖任何数学公理之外的假设。Boris公开了代码，我意识到其中确实包含了全局类域论中一些非常困难的定理的证明。更令我关注的是，Sol在三周内生成了120万行Lean代码，而Lean的数学库mathlib（我参与维护）只有230万行，却花了九年时间编写。这让我深刻意识到，大规模AI生成的数学发展已不可避免。

有限平坦群概形的反例

7月初，我正忙于筹备“形式化费马大定理”研讨会。会上，Logos Research公司提供了自动形式化工具。为了让所有参会者都能实验，我为他们购买了Claude Max订阅（可使用Claude Fable模型）。OpenAI得知后，也为所有参会者提供了ChatGPT Pro的免费访问权限（可使用即将发布的Sol模型）。

为了推进费马大定理的证明，我需要Lean中关于有限平坦群概形的理论。我将一些经典论文上传给Fable和ChatGPT，让它们合作写出一份自然语言的论述。研讨会第一天，Logos指出这份PDF中有一个论断是错误的，并给出了明确的反例。我检查后发现，确实是LLM生成的PDF在描述标准构造时出了错。有趣的是，AI不仅说“不理解这个论证”，而是直接给出了“这个论证是错误的”的证明。

研讨会期间，我与芝加哥大学的Akhil Mathew教授讨论了AI可以研究的问题。他提到了格罗滕迪克的一个老问题：是否每个阶数为n的有限自由群概形都被n消灭？德利涅证明了交换情形，格罗滕迪克证明了基概形是约化时的情形，Schoof和Torti等人证明了更多情形。我认为这是个让AI思考的绝佳问题。

研讨会结束后的第二天（7月11日），Akhil告诉我Sol找到了一个反例，并发来一份12页的PDF。我要求他将整个内容形式化为Lean代码。四小时后，他回复说Fable已经自动形式化了全部内容。我检查了那个1076行的Lean文件，确认它只包含定理后，在我的笔记本上编译运行，总共不到五分钟就验证了：(a) 定理的陈述只使用了mathlib中的概念；(b) 陈述表明存在一个反例；(c) 证明编译通过。这意味着我们有了一个阶数为4、但不被4消灭的群概形反例。我建议Akhil向mathlib提交了这个反例。虽然这解决了一个60年之久的代数几何问题，但到这时，我几乎对这类消息感到麻木了。

模性提升定理的进展

7月14日，我的博士生Andrew Yang告诉我，他利用Sol和Fable等工具，在两周内编写了25万行Lean代码，基本完成了模性提升定理的形式化工作，这对我的费马大定理证明至关重要。

此前，帝国理工的一位教授曾对研究生每月花200美元使用Sol和Fable等模型表示不解。但在与Andrew会面后，我回复他说，在我看来，任何不花这200美元的博士生才是疯狂的。事实上，哈佛大学已经开始为所有博士生、博士后和教职人员免费提供Fable访问权限。

雅可比猜想的反例

Akhil似乎深刻理解了，借助这些强大的AI工具，寻找反例可能是当前最容易取得突破的方向。他与Levent Alpöge讨论了在代数几何中寻找更多反例。12小时前，Levent在X上发帖称，Fable找到了雅可比猜想的一个反例。这是一个著名的、已开放100年的代数几何问题。我今早收到Akhil的私信问“我是不是该再提交一个PR？”，但这次他晚了——Paul Lezeau已经手动形式化了这个反例，并向DeepMind的形式化猜想库提交了PR。由于DeepMind的库已经形式化了该猜想的陈述，验证这个反例变得非常简单。

雅可比猜想被解决了！下一步，人类需要理解这个例子背后的真正原理，从而获得更深刻的数学洞察。这真是令人振奋的时代。

根据评论内容，主要观点和论据总结如下：

观点一：AI辅助数学发现是进步，但并非全新突破 - 支持者认为，AI能高效找到反例，节省人力（评论3：“It saves people wasting time trying to prove something they now know to be false”）。 - 但批评者指出，这本质是计算能力提升和趋势所致，而非根本性变革（评论1：“we now have a lot more compute... it is currently trendy to do so”）。

观点二：人类数学家仍不可或缺 - AI需要人类设计提示和确定搜索方向（评论2：“mathematicians are still needed at crafting prompts, and knowing where to look”）。 - 反例发现可能源于人类此前未系统搜索，而非AI的独创性（评论1：“people just hadn't looked, systematically, for a counterexample”）。

观点三：AI可能带来重大突破，但需谨慎乐观 - 若AI能解决霍奇猜想等千禧年问题，将是重大事件（评论4：“that would be a really big deal”）。 - 但AI目前更多是验证已知领域，而非创造全新数学（评论7：“largely just proving what was already known”）。

观点四：工具本质与人文反思 - AI是工具，突破仍依赖人类数学家（评论9：“Human mathematicians using ChatGPT are breaking boundaries”）。 - 有评论以个人经历说明，不同视角和工具对数学发现同样重要（评论6：“it can be helpful to have people with different tools, hopes, and motivations”）。

平衡总结：多数评论认可AI在数学反例搜索中的效率提升，但强调人类在问题设定、方向判断和创造性思维中的核心作用。AI尚未带来根本性范式变革，但可能加速已知领域的验证，并为未来重大突破铺路。