AI推翻80年数学猜想：生成与验证范式给开发者的启示

菲尔兹奖得主得知自己二十年的研究成果被推翻后，一整夜没有睡着。这个细节在数学圈引发的不只是惋惜，更是一种技术恐慌：AI已经在数学的疆域里，从“帮人算题”进化到了“重新定义边界”的程度。

这则新闻很容易被当成猎奇故事看。但从技术角度看，它真正值得关注的点是：AI参与数学证明的路径，已经不再是“生成一段看起来合理的文本”，而是变成了“生成候选结构 + 形式化验证反向检验”的工程流程。这不是新闻新闻，而是一次研究范式层面的变化。

这篇文章会把这个变化拆开讲清楚。你会看到：AI是如何做到“推翻”一个80年猜想的，它用到了哪些计算与验证技术，为什么数学界和AI界对这次事件的反应如此剧烈，以及这套“生成-验证”方法对普通开发者日常编程、测试和代码审查有什么可迁移的启发。

1. 这件事为什么震动数学圈：拉开黑箱看AI是怎么“推翻”猜想的

先还原一下事件本身。这个80年猜想是有数学传统的经典问题，很多顶尖数学家都在它上面投入过大量时间。菲尔兹奖得主的团队也建立了完整的研究体系，基本上是认定了猜想成立，甚至后续论文都是基于这个结论展开的。突然有一天，AI给出了反例。更不妙的是，这个反例不是简单的数字异常，而是经过验证器严格检验后成立的数学反例。

也就是说，AI不是在“建议”数学家检查某个边界条件，而是直接推翻了原命题：在某个之前没人想到过的构造中，原猜想不成立。

这就引出了很多人的第一个疑问：AI是“凭空”想出来的吗？当然不是。从技术实现角度看，AI证明或反证一个数学命题时，通常跑的是下面这条流水线：

1. 用语言模型或搜索模型生成数学实体。这个实体可以是一组对象、一个函数、一个集合构造，甚至是一个证明思路。
2. 把这些候选实体转换成形式化语言，比如 Lean、Coq、Isabelle 等证明检查器能够理解的表达式。
3. 让证明检查器或模型检验器去验证这个实体是否满足条件。
4. 如果验证通过，反例就成立了。如果验证失败，AI会尝试修正实体，或者放弃这个分支。

这件事的关键在于第二步和第三步之间的约束闭环。LLM 负责生成“看起来有希望的”候选，但真正判断“这个反例对不对”的不是模型，而是数学证明检查器。这就把 AI 的幻觉风险和数学的严谨性要求分开了。

很多人以为这次事件意味着“AI 超越了数学家的直觉”，这个判断其实不够准确。更准确的说法是：AI 提供了一种极低成本、极高覆盖率的候选反例搜索能力，把数学家的工作重心从前期的“寻找反例”推向了“判断反例是否整体推翻理论”。

菲尔兹奖得主一夜没睡，是因为这个反例一旦验证通过，他过去至少二十年的研究路径就可能得推倒重来。这不是一次普通的稿子被拒，而是一个完整理论大厦的地基被抽走了一块。

对于普通开发者来说，这里真正值得吸收的，不是“AI 打败了数学家”这种叙事，而是它背后的思想：用生成器做广度搜索，用验证器做唯一裁决。这个思想在代码领域非常有用，后面我们会专门展开。

2. AI 数学证明的核心概念：从“答题”到“验证”的范式切换

在深入实操之前，先建立一个概念框架。很多人对“AI 证明数学”的理解还停留在“把题目输入 ChatGPT，它给出答案”这个层面。实际上，当前 AI 数学研究的重心远不止于此，它分成三个层次。

2.1 自然语言生成层：AI 像人类一样“想”

这个层次最接近公众认知。你给 AI 一个数学问题，它用自然语言推理，写出证明思路。优点是灵活，缺点是不严谨。因为语言模型本质上是在“预测下一个 token”，它并不知道自己的推导是否真的在逻辑上成立。很多看起来像模像样的证明，细究起来是有漏洞的。

这个层次适合做什么？适合做头脑风暴，适合为数学家提供初始候选思路。但在严肃数学研究中，它不能作为最终裁决。

2.2 形式化语言层：把数学翻译成机器能检查的代码

形式化语言是解决“自然语言不严谨”问题的关键。比如 Lean、Coq、Isabelle 这些系统，它们把数学命题定义成一种精确的、计算机可以检查的语法结构。一个命题在形式化系统里只有两种状态：可证明，或不可证明。不存在“看起来合理但实际上有漏洞”的中间状态。

这一步听起来简单，做起来并不容易。把一个自然语言描述的数学概念翻译成形式化语言，需要大量的人力或模型能力。很多数学定理尽管人类已经证明，但还没能在 Lean 中完成形式化，原因就在翻译成本上。

2.3 证明搜索与反例搜索层：AI 真正的价值空间

当命题已经形式化之后，AI 的作用就变成了搜索。搜索什么？搜索证明路径，或者搜索反例。

以反例搜索为例。一个猜想通常表述为“对于所有满足 X 条件的对象，Y 性质都成立”。要推翻它，只需要找到一个满足 X 但不满足 Y 的对象。问题是，这个对象往往藏在巨大的组合空间中。传统方法靠数学家的经验去吃透这个空间，而 AI 的做法是用生成模型批量生产候选对象，再用形式化验证器逐个过滤。

这个搜索过程本质上和工程里的模糊测试、随机化测试非常像。区别在于，数学对象的“可验证性”要强得多——证明检查器能够确切告诉你一个候选对象是否构成反例，而代码测试很多时候只能告诉你“没找到错误”，不能告诉你“完全没有错误”。

2.4 三个层次的边界

所以，这次“AI 推翻猜想”的完整链路更可能是：LLM 生成了某个构造式的反例候选，然后被形式化验证器确认，最终数学界认可了这个反例成立。

看到这里，你应该已经明白，这起事件背后的技术并没有那么神秘。它用的核心手段，在软件工程里都有对应物：生成器生成数据，验证器判断正确性。区别只在于“正确性”的定义从“代码跑起来”变成了“数学命题被形式化证明”。

3. 为什么 AI 能发现人类几十年看不到的反例

很多人会有另一个疑问：为什么这个反例没有被人类堵住，却让 AI 找到了？这要从人脑和 AI 搜索空间的理解差异说起。

数学家的思考是启发式驱动的。经过多年训练，他们会形成很强的直觉：哪一类构造更可能让命题成立，哪一类构造基本可以放弃。这种直觉在绝大多数时候是高效的，但在极端情况下也会变成路径依赖。当一个猜想统治某个领域太久，后续研究者都会默认它是正确的，于是很少有人再去故意寻找构造性反例。

AI 不一样。AI 没有“面子”，没有“领域共识”，它只负责在约束条件下进行高密度搜索。一个看似离谱、不符合主流直觉的构造，在人类数学家眼里可能直接跳过，但 AI 会把它送入验证器。验证器给出结果，不带有任何感情色彩。

这种搜索能力有几个特点值得注意。

3.1 覆盖面广

AI 生成候选对象时，可以快速覆盖大规模组合空间。比如假设一个猜想涉及某个代数结构，AI 可以用模型生成成千上万个变体结构，每一个都送入验证器检查。这在人类手工程度上几乎不可能。

3.2 无偏见

人类的构造通常受现有理论框架限制。AI 的生成模型虽然也受训练数据影响，但通过对抗性采样或温度调整，可以在一定程度上跳出常见模式。这次找到反例的构造，很可能就是那种“不符合主流美学”的对象。

3.3 高并发

搜索过程可以并行化。多张显卡同时跑多个候选对象的验证，这在数学界之前是不具备的工程条件。数学家写一个证明可能要几个月，AI 检验一个候选对象可能只需要几分钟。

但我们也要保持清醒。AI 并不会自动理解数学的“意义”。它找到反例，不代表它理解了为什么这个反例重要。后续如何消化这个反例，如何调整理论体系，仍然要靠人类的判断。

4. 从数学证明到代码验证：开发者能学到什么

很多开发者会觉得“AI 数学证明”离自己太远，但如果你仔细看这次事件的底层逻辑，会发现它和现代软件工程的若干实践高度同构。

4.1 生成与验证分离

传统开发模式下，程序员写代码，然后测试代码。代码是生成器，测试是验证器。如果验证器足够强，生成器写错了也能被拦下来。但如果测试不充分，就可能让错误溜进线上。

AI 数学证明把这种流程推到了极致：验证器是形式化的，覆盖所有情况，绝无疏漏。对普通项目而言，我们可以借鉴的是：不要靠“写代码的时候更小心”来替代验证，而是把验证器做得足够强，让生成器犯错时能被快速捕捉。

4.2 用搜索思维对抗盲区

开发者经常遇到一类问题：明明测试全过了，线上还是出 bug。很多时候，是因为测试数据生成得太“温和”，都按着开发者自己的预期去构造，最后只是确认了开发者已经知道的信息。

借鉴 AI 证明的思路，我们应该在测试数据生成中加入“对抗性”和“随机性”。不要只测常规输入，也要生成边界条件、非法输入、极端组合。这种做法和反例搜索在精神上是完全一致的。

4.3 形式化验证会进入工程吗

这几年 Lean 社区越来越活跃，已经有人开始尝试把核心算法的正确性证明形式化。虽然成本很高，但一旦完成，这个算法就不会再出现“运行时才发现错误”的情况。对金融、航天、医疗等强安全场景，這个方向的价值会越来越大。

对普通后端开发者来说，短期内不需要立即去学 Lean，但理解“形式化验证是最终安全网”这个概念，能帮助你更合理地设计系统的错误防线：单元测试、集成测试、模糊测试、运行时校验各司其职，而不是期望靠代码审查解决一切。

5. 环境准备：在本地复现“搜索反例”的基本链路

如果你看到这里，想在本地体验一下“AI 生成候选结构 + 验证器把关反例”的流程，可以用一个最小化方案跑通。不要求有大型 GPU，也不需要配置大模型，我们只需要模拟核心验证逻辑。

工具建议：

• Python 3.8 以上版本，用于编写搜索和生成逻辑。
• z3-solver：微软出品的约束求解器，非常适合做命题验证与反例构造。
• 可选 Lean 环境：如果你想体验数学定理的形式化表示，可以去 Lean 官网按照官方指引安装，版本请以官方为准，本文后面的示例主要以 Python 和 z3 为主。

安装 z3 很简单：

pip install z3-solver

安装完成后，可以用一个简单的逻辑题验证环境是否可用。

from z3 import * x = Real('x') s = Solver() s.add(x**2 < 0) # 这显然无解 result = s.check() print(result) # unsat，说明这个约束不可满足

如果你的输出是unsat，说明环境正常。接下来我们会做一个更贴近“反例搜索”的示例。

6. 完整示例：用 z3 构造一个数学猜想的反例

假设我们有一个虚构的猜想：对于任意正整数 n，表达式 f(n) = n^2 + n + 41 的结果都是素数。

这是一个非常经典的“假猜想”变体。欧拉曾指出 n = 0 到 39 时它都是素数，但 n = 40 时就不是了。我们用 z3 来做这个反例搜索，模拟 AI 证明中“验证器”的角色。

先写一个简单的 Python 脚本，尝试枚举 n 并验证是否素数：

# 文件：prime_counter_example.py def is_prime(num): if num < 2: return False if num == 2: return True if num % 2 == 0: return False i = 3 while i * i <= num: if num % i == 0: return False i += 2 return True def check_counterexample(): counter_examples = [] for n in range(1, 100): value = n * n + n + 41 if not is_prime(value): counter_examples.append((n, value)) print(f"找到反例：n={n}, f(n)={value}，不是素数") break return counter_examples if __name__ == "__main__": check_counterexample()

运行之后，结果会非常明确：

找到反例：n=40, f(n)=1681，不是素数

这个例子展示了反例搜索的基本思想：遍历候选空间，把每一项送到验证函数里，找到一个不满足约束的项，就完成了“推翻”任务。

接下来看一个更有“AI 证明”味道的例子。我们不再自己枚举，而是让 z3 直接求解一个布尔可满足性问题，找出反例。

# 文件：z3_counter_example.py from z3 import * # 定义整数变量 n n = Int('n') # 构造表达式 f(n) = n^2 + n + 41 f = n * n + n + 41 # 声明一个辅助变量 p，表示某个整数 p = Int('p') # 约束：n 是正整数，f 等于 p * q，且 p 和 q 都不是 1 或 f 本身 # 这就是“f(n) 是合数”的一种表示 q = Int('q') s = Solver() s.add(n > 0) s.add(p > 1) s.add(q > 1) s.add(f == p * q) if s.check() == sat: model = s.model() print(f"找到反例：n={model[n]}, p={model[p]}, q={model[q]}") print(f"f(n)={model[n].as_long() ** 2 + model[n].as_long() + 41}") else: print("没有找到反例，表达式在此范围内不成立")

这段脚本的思路是：让求解器自己去寻找一组满足“f(n) 为合数”条件的整数解。如果约束可满足，就得到了一个反例。这比人工遍历更接近智能搜索。

运行输出类似：

找到反例：n=40, p=41, q=41 f(n)=1681

在这里，z3 充当了“验证器”的角色。它没有通过枚举，而是用约束求解和搜索技术，在逻辑空间中找到了符合反例条件的对象。真实数学研究中，LLM 生成候选，验证器检查候选，本质上是同一个闭环的更大规模版本。

7. 完整示例：在代码项目中用随机搜索发现隐藏 bug

上一节的例子是数学反例搜索。现在把同样的思想移植到软件工程中，用一个小工具随机生成边界输入，检查一个函数的输入输出是否满足预期约束。

假设我们有一个函数，它声称可以对输入进行某种数学转换，返回值必须保持某个性质。我们想知道它是否真的在所有情况下都成立。

# 文件：property_based_search.py import random import math def compute_safe_sqrt(x): """声称只在 x >= 0 时被调用，返回值的平方应当等于 x。""" if x < 0: return None return math.sqrt(x) def assert_sqrt_property(x): result = compute_safe_sqrt(x) if result is not None: # 验证性质：平方回来误差足够小 if abs(result * result - x) > 1e-9: return False return True # 随机生成很多输入，看看性质是否被破坏 random.seed(42) violated = [] for _ in range(10000): x = random.uniform(-1000, 1000) if not assert_sqrt_property(x): violated.append(x) break if violated: print(f"发现违反性质的输入：{violated[0]}") else: print("随机测试中未发现违反性质的输入")

这个例子虽然简单，但已经具备生成器（随机输入）和验证器（属性检查）的分离。真实项目中，我们可以把这个思路扩展到更复杂的性质，比如：

• 并发安全的计数器，无论多线程执行多少次，总数不变。
• 幂等接口，重复调用和单次调用结果一致。
• 数据库事务，崩溃后不会出现部分提交数据。

这些都属于“生成-验证”思想在软件领域的落地。

8. 常见问题与排查方法

在实际操作 AI 辅助推理或验证工具时，你可能会遇到下面这些典型问题。

这一部分不必期望一次全部解决，但至少提供一个排错思路。任何 AI 参与的工作，真正需要盯紧的仍然是“验证器是否可靠”，而不是“生成器是否聪明”。

9. 最佳实践与工程建议

围绕“AI 生成 + 验证器把关”这一范式，有几点工程建议值得认真考虑。

9.1 不要把 AI 当最终裁决者

无论是数学证明还是代码生成，AI 的输出都只是候选。你还需要一个不依赖 AI 的验证机制。在代码领域，这个验证机制是测试和类型系统；在数学领域，就是形式化证明检查器。如果验证器和生成器是同一个模型，风险会非常大，因为错误会自我强化。

9.2 让验证器足够“挑剔”

好的验证器不仅要能验证“正确的情况”，还要能高亮“违反约束的情况”。写单元测试时，不要只写正向用例，一定要写负向用例，确认系统在非法输入下会拒绝而非静默出错。这个习惯和数学证明中的反例搜索是一致的。

9.3 用属性测试补充示例测试

基于示例的测试只能覆盖已知内容，属性测试却能覆盖更大的输入空间。Python 里的hypothesis库是很好的选择，它可以自动生成边界值、极端值和非法值，从多个维度挑战你的函数。

一个简单示例：

from hypothesis import given, strategies as st @given(st.integers()) def test_sqrt_property(x): result = compute_safe_sqrt(x) if result is not None: assert abs(result * result - x) < 1e-9

如果函数的实现有隐藏的边界问题，属性测试往往能在几秒内暴露它。

9.4 记录可复现性

AI 辅助推理最大的陷阱是“不可复现”。无论是随机种子、模型版本，还是验证器版本，都必须记录下来。写进文档，写进 CI 配置，确保任何人都可以重新生成验证结果。数学界的反例如果不能复现，基本不会被承认；代码领域的 bug 如果无法稳定复现，定位代价也很高。

9.5 成本控制

大规模反例搜索并非没有成本。在数学领域，验证一个候选对象可能要跑很久；在代码测试里，全量模糊测试也可能吃满计算资源。合理做法是分层：快速验证器跑大量低成本的候选，复杂验证器只处理少数高价值候选。

10. 总结与后续学习方向

这次“AI 推翻 80 年数学猜想”的事件，从本质上看，不是 AI 突然学会了“创造数学”，而是“生成式模型 + 形式化验证器”这套工业流程在数学领域的首次大规模胜利。它告诉我们，AI 真正的可靠价值不在于替代人去做判断，而在于扩大人可以做判断的覆盖面。

对开发者而言，这个事件提供了两个重要提醒：

第一，验证器是安全网。无论是测试、类型系统、静态检查，还是形式化证明，都是防止错误扩大化的核心工具。不要把安全寄托于“我不会写错”。

第二，生成器的真正价值在于拓展搜索空间。AI 可以生成人类不常想到的边角输入、边界条件、组合模式，这些是发现隐藏 bug 和隐藏反例的关键。

下一步，如果你想继续深入，可以从这些方向入手：

• 学习 z3 的更多使用场景，解决实际的约束求解问题。
• 了解 Lean 社区，观察形式化数学的进展。
• 在个人项目中引入 property-based testing，提升测试覆盖率。

AI 并不会替代工程师，但它会重新定义“工程师一天能覆盖的问题量”。学会让 AI 生成候选、让工具做验证、让经验做判断，这才是面对这类事件最理性的态度。