摘要：AI参与数学研究的第一批规模化入口，未必是独立写出长篇证明，而是帮助研究者寻找反例、测试猜想、发现遗漏条件，并把候选结果交给Lean等形式化系统验证。
2026年7月20日，Xena Project发布了一篇题为《Human mathematicians are being outcounterexampled》的文章。
文章记录了几件连续发生的事情：OpenAI模型推翻了离散几何中的一个长期猜想；AI工具找到了格罗滕迪克提出的一项问题的反例；一些数学家开始把尚未解决的问题主动交给模型，要求它先尝试寻找例外情况。
这些案例把AI参与数学研究的一条路径摆到了台面上。
模型未必需要先完成一篇几十页的证明。它也可以从猜想的薄弱位置入手，寻找一个满足前提、却违反结论的对象。只要这个对象成立，猜想就被推翻了。
一个反例为什么能够结束一个猜想
很多数学猜想都带有“所有”“任意”“在任何情况下”这样的条件。
例如，有人提出：
所有连续函数都可导。
要证明这句话，需要覆盖所有连续函数。要推翻它，只需找到一个连续但不可导的函数。绝对值函数在零点连续，却不可导，因此足以否定这个命题。
反例的力量来自这里。
面对一个普遍性结论，证明需要建立完整逻辑链条，反例只需要找到一个有效例外。寻找过程依然可能很难，但验证对象通常更加具体。
数学研究中，大量时间花在判断一条猜想是否值得继续推进。一个研究人员可能根据若干计算结果、特殊情形或直觉提出猜想，随后投入数月寻找证明。若猜想本身存在一个很隐蔽的反例，这些工作可能长期围绕错误方向展开。
反例搜索相当于给猜想做压力测试。研究人员提出结论后，先让程序搜索边界情况、极端参数和复杂结构。若没有发现问题，再进入长期证明阶段。
OpenAI模型推翻了一个80年的判断
2026年5月20日，OpenAI公布了一项离散几何结果。
问题源自数学家保罗·埃尔德什1946年提出的单位距离问题：在平面上放置若干个点，最多能够形成多少对距离恰好为1的点？
此后几十年里，数学界普遍认为，以方格结构为基础的构造已经接近最佳结果。OpenAI内部模型给出了一组新的构造，证明单位距离对的数量可以获得固定多项式级别的提升，从而推翻了这一长期判断。OpenAI称，相关证明经过一组外部数学家检查。
这项工作的一个特点，是模型没有沿着主流方向继续尝试证明已有上界。它把主要精力放在构造反例上。
模型将代数数论中的类域塔和Golod-Shafarevich理论引入离散几何，用一组来自另一个数学领域的工具，构造出超过原有预期的点集。数学家熟悉这些数论工具，也熟悉单位距离问题，但此前很少有人把两者联系起来。
模型能够检索、组合和尝试大量跨领域路径。只要其中一条路径能够产生具体构造，后续工作便可以围绕这个对象展开。
从“可能不对”变成“这里有一个反例”
7月初，Xena Project组织了一次费马大定理形式化研讨活动。
活动准备阶段，研究人员把有限平坦群概形相关材料交给AI工具整理。模型发现其中一条表述存在问题，并给出了明确反例。作者检查后确认，原文确实写错了。
这类能力在研究中很实用。
阅读一篇复杂论文时，人类常会感觉某个步骤“不太对”“缺了条件”或“结论似乎过强”。从怀疑走到否定，还需要构造对象并完成计算。
AI工具可以持续尝试这些工作。它不会因为一个方向缺乏名气、形式丑陋或者计算过程繁琐而主动放弃，也不在意反例是否符合数学家的审美。
对于检查论文、验证中间引理和测试猜想，这种耐心有较高价值。
一个60年前的问题，四小时完成形式化验证
在同一次研讨活动中，芝加哥大学数学家Akhil Mathew提出了格罗滕迪克留下的一项问题：一个阶为n的有限局部自由群概形，是否一定被n消去？
此前，数学家已经在交换情形、约化基底和其他特殊条件下证明了相应结果，但一般非交换情形仍未解决。
AI工具随后找到一个阶为4、却不被4消去的群概形。研究人员收到的是一份12页的非形式化材料。
Xena Project作者没有直接接受这份材料，而是要求把全部论证写成Lean代码。四小时后，系统生成了一份1076行的Lean文件。作者在本地编译通过后确认，这个文件证明了一个满足形式化陈述的反例。
相关代码随后被提交到数学库mathlib。提交说明列出了底环、坐标代数、Hopf代数结构以及第四卷积幂不等于单位映射的计算，并披露该构造与形式化过程使用了OpenAI和Anthropic的AI工具。
这里出现了一套较完整的科研流程：
数学家选择问题；
模型搜索候选反例；
另一个模型把论证转成Lean代码；
Lean检查每一步是否符合形式规则；
人类检查形式化陈述是否准确表达原问题；
研究人员再分析这个反例为什么成立。
在这套流程中，生成、验证和解释被分开处理。
Lean解决了模型最难处理的可信度问题
大语言模型可以写出结构完整、语气自信的数学证明，却可能在某一步使用不存在的定理，遗漏必要条件，或者悄悄改变问题定义。
只阅读自然语言，很难快速排除这些问题。
Lean是一种形式化证明系统，也是一门编程语言。数学定义、定理和推理步骤需要按照明确语法表达，证明只有通过Lean内核检查，才能被系统接受。
模型可以负责提出反例和编写证明代码，Lean负责机械验证。
2026年一项关于形式化反例生成的研究，把任务分成两个阶段：模型先通过自然语言推理提出候选反例，再生成对应的Lean证明。只有形式证明通过检查，候选对象才被视为有效。
研究团队还设计了一种训练方法。他们从已被证明的定理中删除关键假设，使原定理失效，再要求模型寻找反例。通过这种“删条件”的方式，团队合成了57.5万个反例训练样本。经过训练的模型，在三个新建基准上的首次生成成功率，相对最强基线提高了47%至74%。
这说明寻找反例可以被单独训练。
此前数学模型的主要目标是证明一个命题成立。新方法开始训练模型判断命题何时不成立，以及缺少哪一个条件会导致结论崩溃。
机器为什么适合做反例搜索
数学家寻找反例时，往往依靠经验。
他们会检查最小规模、退化情形、边界值、非交换结构、奇异对象和不符合直觉的构造。这些方法有效，却受限于个人知识范围和时间。
机器有几项适合这类任务的条件。
第一，可以大规模枚举。有限群、图结构、整数序列、矩阵和组合对象都可以按照一定范围生成，然后逐个测试猜想。
第二，可以持续尝试不美观的构造。人类倾向于寻找简洁、对称、有解释力的对象。第一个有效反例可能非常复杂，也可能由一组看似随意的参数组成。机器更容易接受这种搜索结果。
第三，可以连接不同数学领域。一个离散几何问题可能需要代数数论工具，一个群概形问题可能落到具体环和Hopf代数计算。模型接触过大量数学文本，能够提出一些研究者平时不会优先考虑的组合。
第四，可以与符号系统配合。SAT求解器、SMT求解器、计算机代数系统和证明助手已经能够搜索有限反模型、验证等式和检查逻辑。大语言模型可以负责理解自然语言问题、设计搜索路径和调用这些工具。
第五，可以并行测试大量猜想。一项2026年的研究让AI形式化证明智能体处理353个开放的埃尔德什问题和492个OEIS猜想，分别解决了9个和44个。研究表明，把模型生成与Lean验证循环结合，已经可以在开放数学问题上开展批量搜索。
科研价值可能先体现在“减少错误方向”
AI参与数学研究常被描述为“解决世纪难题”。
这类目标吸引注意力，却不一定是最早形成规模的应用。
一个更常见的工作场景是：
检查论文中的引理有没有反例；
测试新猜想是否遗漏条件；
扫描数据库中的未决问题；
比较多个定理表述之间的差异；
检查形式化题库是否写错；
在正式证明前排除大量失败方向。
形式化数学基准也存在陈述错误。2026年一项针对Lean证明基准的审计研究，在约一万个问题版本中发现了大量潜在缺陷，其中包括可被具体反例直接推翻的陈述、互相矛盾的假设、除零和定义域处理问题。
这与软件开发很接近。
程序员不会等系统上线后才检查代码是否运行。测试会提前覆盖异常输入、边界情况和错误路径。数学猜想也可以增加类似环节。
一条命题进入长期研究前，先经过自动反例搜索、有限范围计算和形式化检查。机器没有找到反例，不代表命题成立；一旦找到有效反例，研究方向可以立即调整。
形式化通过也不代表工作已经结束
Lean能够证明一段形式代码成立，但它检查的是代码中的陈述。
若形式化过程误解了原问题，Lean可能严谨地证明了另一个命题。
因此，至少需要检查三件事：
形式定义是否符合数学家的通常理解；
形式命题是否完整保留了原猜想的条件；
代码是否引入了额外公理、空假设或特殊定义。
形式化基准审计已经发现，除零处理、自然数截断减法、定义域缺失和无效假设，都可能让一个程序可证明的结论偏离数学原意。
另外，一个反例可以推翻猜想，却不一定立即带来理解。模型可能给出一个结构庞大、参数复杂的对象。人类知道它成立，却暂时说不清它为什么值得关注，也不知道如何把它推广为一套方法。
Xena Project在介绍群概形反例时也强调，后续工作是理解这个例子的结构，提取能够帮助人类继续研究的数学见解。
科研论文需要的内容通常超过“答案正确”。研究人员还要解释：原猜想为什么会失效；反例利用了哪个遗漏条件；哪些特殊情形仍然成立；能否提出更准确的新猜想；这一结构是否会影响其他问题。
这些工作依赖领域知识和数学判断。
数学家的工作会多出一个“猜想测试”阶段
未来的数学研究流程可能会增加一个固定环节。
研究人员提出猜想后，先把它交给多个系统处理：
大语言模型分析潜在薄弱点；
程序枚举小规模对象；
计算机代数系统完成符号运算；
反例生成器测试极端条件；
Lean、Isabelle等证明助手检查形式结果；
人类审核问题表述和数学意义。
通过这一轮检查的猜想，才进入长期证明工作。数学家也可以一次提出一组相关命题，让机器先筛掉明显错误的部分，再集中精力研究剩余问题。
这会改变研究资源的分配方式。过去，一个猜想是否值得投入，往往依赖提出者的声望、个人直觉和少量计算。自动反例搜索可以增加一层可重复的技术检查。
对数学教育也有类似价值。学生写完证明后，系统不只告诉他“证明过程不完整”，还可以给出一个满足前提却违反结论的具体对象。学生能够直接看到自己遗漏了哪个条件。
从证明答案，转向管理研究过程
AI寻找反例的意义，不只体现在推翻几个著名猜想。
它提供了一种研究管理工具。
一项猜想可以先接受机器测试；一条复杂论证可以被逐段检查；一个形式化数据库可以持续扫描；研究人员能够更快判断哪些方向已经失效，哪些问题值得继续投入。
模型负责扩大搜索范围，形式化系统负责守住逻辑边界，数学家负责选择问题并解释结果。这套组合已经可以处理部分开放问题，也能发现论文表述和数学数据库中的错误。
对科学研究而言，尽早发现一条路走不通，本身就是进展。
一个有效反例可以节省数月甚至数年的证明工作，还可能指出原猜想缺少的关键条件。沿着这个条件修改问题，新的定理和研究方向才有机会出现。
AI进入数学研究后，最先被规模化的能力，可能不是连续写出漂亮证明。它会先成为一台不知疲倦的猜想测试机。
参考资料
Xena Project：《Human mathematicians are being outcounterexampled》，2026年7月20日。
OpenAI：《An OpenAI model has disproved a central conjecture in discrete geometry》，2026年5月20日。
Zenan Li等：《Learning to Disprove: Formal Counterexample Generation with Large Language Models》，2026年3月。
George Tsoukalas等：《Advancing Mathematics Research with AI-Driven Formal Proof Search》，2026年5月。