麦克斯韦猜想被推翻：GPT给出反例震动数学圈

一则震动数学圈的消息

近日，Hacker News 上一篇标题为《The Maxwell Conjecture Is False (GPT 5.6 Sol)》的帖子引发了热烈讨论，短时间内获得了 65 个点赞和 31 条评论。帖子的核心主张相当惊人：一个长期悬而未决的数学猜想——麦克斯韦猜想（Maxwell Conjecture）——被证明是错误的，而给出反例的，据称是大型语言模型的迭代版本「GPT 5.6」。

这条消息之所以引起广泛关注，不仅在于数学结论本身，更在于它触及了当下最敏感的话题：AI 是否已经具备解决前沿数学问题的能力？ 如果这个反例成立，它将成为 AI 在纯数学研究中做出实质性贡献的又一个标志性案例。

什么是麦克斯韦猜想

猜想的起源与表述

麦克斯韦猜想源自静电学与位势论（Potential Theory）领域，最初可追溯到物理学家詹姆斯·克拉克·麦克斯韦（James Clerk Maxwell）对静电场平衡点的研究。其中一个经典表述涉及 $n$ 个点电荷所产生的电场中，平衡点（即电场强度为零的点）的最大数量问题。

位势论是数学物理中的一个经典分支，研究满足拉普拉斯方程或泊松方程的函数（即调和函数或位势函数）的性质。在静电学中，点电荷产生的电势可以表示为距离的反比函数，而多个点电荷的总电势是各单独电势的线性叠加。电场是电势的负梯度，因此寻找电场平衡点等价于寻找电势函数梯度为零的临界点。这一问题虽然起源于物理学，但其本质是纯粹的数学分析问题，涉及有理函数零点的计数与分布。

麦克斯韦在1873年出版的经典著作《电磁学通论》（A Treatise on Electricity and Magnetism）中，系统讨论了点电荷系统的平衡点问题。他基于物理直觉提出，$n$ 个点电荷产生的静电场，其平衡点的数量不会超过 $(n-1)^2$。这个看似简洁的上界猜想，长期以来在位势论和代数几何领域缺乏严格证明——数学家甚至连三个点电荷的一般情形都难以完全厘清。此后一百多年来，该猜想吸引了数学物理、代数几何和拓扑学等多个领域的研究者关注，但进展始终缓慢。它属于那种「陈述简单、证明困难」的经典数学难题。

为何长期难以证明

这类问题的困难在于，平衡点的计数涉及多元非线性方程组的解的结构分析，需要结合代数几何、拓扑学以及实分析的工具。

具体而言，在三维空间中，$n$ 个点电荷产生的电场为零的条件给出三个非线性方程，每个方程的分母涉及所有电荷到待求点的距离。消除分母后得到的多项式方程组，其次数随电荷数量快速增长。Bézout 定理给出了解数的一个粗糙上界，但远大于麦克斯韦猜想的 $(n-1)^2$。而要得到精确的上界，需要分析方程组在无穷远处和退化情形下的行为，这涉及代数几何中的交叉理论（intersection theory）、Morse 理论以及实代数几何的精细工具。

要构造一个反例——即找到某种电荷配置使得平衡点数量超出预期上界——往往需要极其精巧的构造性思维和大量的符号计算，这对人类数学家而言也是巨大的挑战。

AI给出反例意味着什么

从辅助工具到数学问题解决者

如果 GPT 5.6 确实独立或半独立地构造出了推翻麦克斯韦猜想的反例，这标志着 AI 在数学研究中的角色正在发生质变。过去，AI 更多扮演文献检索、符号计算或猜想生成的辅助角色；而构造一个推翻长期猜想的反例，则需要真正的数学洞察力与创造性——这曾被认为是人类数学家的专属领地。

近年来 AI 在数学领域已有多次突破性表现：

• DeepMind 的 AlphaProof 在国际数学奥林匹克中取得银牌水平成绩。AlphaProof 将语言模型与 AlphaZero 式的强化学习相结合，在形式化数学证明语言 Lean 中进行搜索和推理。在2024年国际数学奥林匹克（IMO）中，它解决了6道题中的4道，达到银牌水平，这是 AI 首次在顶级数学竞赛中展现出接近人类精英选手的能力。
• FunSearch 发现了组合数学中的新构造。FunSearch 通过大语言模型与进化搜索的结合，在组合数学的 cap set 问题上发现了超越已知最优构造的新结果，该成果发表在《Nature》上。这两个项目共同标志着 AI 在数学领域从「辅助计算」向「独立发现」的转变。
• 各类大模型开始参与形式化证明的辅助工作

「AI 推翻麦克斯韦猜想」如果属实，将是这一趋势的重要延续。

社区保持审慎态度

Hacker News 的评论区对此保持了技术社区特有的审慎。AI 给出的数学「证明」或「反例」需要经过同行严格验证——尤其要通过形式化证明工具（如 Lean、Coq）或独立数学家的复核，才能真正被学界接受。

Lean 和 Coq 是当前最主流的两种交互式定理证明器（Interactive Theorem Prover）。Lean 由微软研究院的 Leonardo de Moura 开发，近年来因其活跃的数学形式化社区 Mathlib 而备受关注——Mathlib 已经形式化了数十万条数学定理，涵盖从本科到研究生水平的广泛数学内容。Coq 则历史更为悠久，曾用于验证四色定理的计算机证明。形式化证明的核心价值在于：每一步推理都由计算机内核检查，不可能存在逻辑跳跃或隐含假设，这使得形式化验证成为 AI 数学产出的终极仲裁机制。

AI 生成内容存在「幻觉」（hallucination）的风险，一个看似严密的论证中可能隐藏着微妙的逻辑跳跃或计算错误。大语言模型的幻觉在数学领域有其特殊的表现形式：与事实性幻觉（如编造不存在的历史事件）不同，数学幻觉往往表现为看似合理但实际不成立的引理引用、不经意间使用了未经证明的中间结论、维度或边界条件的微妙错误，以及在关键步骤进行了不等价的变换。这类错误往往比明显的错误更加危险，因为它们可能骗过非专业审稿人甚至部分专家。2023年曾有多起 AI 生成的数学「证明」在初步审核后被发现存在根本性错误的案例，这使得学界对 AI 数学声明的验证流程更加重视。

因此，在缺乏权威验证之前，任何「AI 攻克某猜想」的声明都应被视为待验证的候选结果，而非最终定论。

这一事件的深层启示

数学的可验证性为AI参与提供保障

这一事件再次凸显了数学中「可验证性」的核心价值。与其他领域不同，数学结论可以通过形式化系统进行机器验证——这恰恰为 AI 参与数学研究提供了天然的安全网。无论证明由人还是 AI 给出，只要能被形式化并通过验证，其正确性就是确定的。如果一个证明或反例能在 Lean 中通过类型检查，其正确性在逻辑上就是确凿无疑的。

这意味着，AI 在数学领域的贡献比在其他领域更容易被客观评估。未来我们很可能会看到一种新型协作范式：AI 提出猜想或构造反例，人类或机器完成验证。这种分工充分利用了 AI 在搜索空间探索上的计算优势和形式化系统在逻辑验证上的严格性，有望大幅加速数学研究的进程。

模型迭代速度的信号

帖子标题中「GPT 5.6」这样的版本号本身也值得关注——它暗示着模型的快速迭代，以及数学推理能力的持续跃升。无论这个具体版本号是否准确，它反映出社区对下一代 AI 模型数学能力的期待正在快速升温。从 GPT-4 展现出的初步数学推理能力，到 o1、o3 系列模型在复杂推理任务上的显著提升，再到如今传闻中 GPT 5.6 在前沿数学问题上的突破，大语言模型的数学能力正以超出许多人预期的速度演进。

结语

「麦克斯韦猜想被 AI 推翻」目前仍是一个需要审慎对待的社区讨论话题。它可能是 AI 数学能力的又一个里程碑，也可能是需要进一步验证的候选结果。

但无论最终结论如何，这一事件传递出一个清晰的信号：AI 正从数学研究的边缘走向核心。在可验证性的保障下，人类数学家与 AI 的协作，或许将成为未来解决重大数学难题的常态。真正的问题已经不再是「AI 能否做数学」，而是「我们如何验证并善用 AI 的数学产出」。