菲尔兹奖得主得知自己二十年的研究成果被推翻后一整夜没有睡着。这个细节在数学圈引发的不只是惋惜更是一种技术恐慌AI已经在数学的疆域里从“帮人算题”进化到了“重新定义边界”的程度。这则新闻很容易被当成猎奇故事看。但从技术角度看它真正值得关注的点是AI参与数学证明的路径已经不再是“生成一段看起来合理的文本”而是变成了“生成候选结构 形式化验证反向检验”的工程流程。这不是新闻新闻而是一次研究范式层面的变化。这篇文章会把这个变化拆开讲清楚。你会看到AI是如何做到“推翻”一个80年猜想的它用到了哪些计算与验证技术为什么数学界和AI界对这次事件的反应如此剧烈以及这套“生成-验证”方法对普通开发者日常编程、测试和代码审查有什么可迁移的启发。1. 这件事为什么震动数学圈拉开黑箱看AI是怎么“推翻”猜想的先还原一下事件本身。这个80年猜想是有数学传统的经典问题很多顶尖数学家都在它上面投入过大量时间。菲尔兹奖得主的团队也建立了完整的研究体系基本上是认定了猜想成立甚至后续论文都是基于这个结论展开的。突然有一天AI给出了反例。更不妙的是这个反例不是简单的数字异常而是经过验证器严格检验后成立的数学反例。也就是说AI不是在“建议”数学家检查某个边界条件而是直接推翻了原命题在某个之前没人想到过的构造中原猜想不成立。这就引出了很多人的第一个疑问AI是“凭空”想出来的吗当然不是。从技术实现角度看AI证明或反证一个数学命题时通常跑的是下面这条流水线用语言模型或搜索模型生成数学实体。这个实体可以是一组对象、一个函数、一个集合构造甚至是一个证明思路。把这些候选实体转换成形式化语言比如 Lean、Coq、Isabelle 等证明检查器能够理解的表达式。让证明检查器或模型检验器去验证这个实体是否满足条件。如果验证通过反例就成立了。如果验证失败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 三个层次的边界层次核心工具输出严谨度适用场景自然语言推理LLM证明思路、反例描述低头脑风暴、候选生成形式化语言Lean / Coq / Isabelle形式化命题与证明高数学定理入库、可验证研究搜索与验证自动定理证明器 / 求解器证明路径、反例高检查猜想、生成反例、扩展证明库所以这次“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()运行之后结果会非常明确找到反例n40, 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(ff(n){model[n].as_long() ** 2 model[n].as_long() 41}) else: print(没有找到反例表达式在此范围内不成立)这段脚本的思路是让求解器自己去寻找一组满足“f(n) 为合数”条件的整数解。如果约束可满足就得到了一个反例。这比人工遍历更接近智能搜索。运行输出类似找到反例n40, p41, q41 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 辅助推理或验证工具时你可能会遇到下面这些典型问题。问题现象可能原因排查方式解决方案z3 返回 unsat但人工觉得应该有解约束条件过于严格或变量域设置错误打印当前约束并逐个注释确认哪个约束导致不可满足放宽约束比如排除 n0或增加变量范围限制随机测试没有发现 bug但线上出问题测试数据生成过于温和没有覆盖极端输入检查随机数种子和取值边界添加符合业务场景的对抗样本引入模糊测试工具如 hypothesis 或 libFuzzerAI 生成的证明看起来合理但验证器报错形式化表达与自然语言意图不一致仔细检查变量定义、假设条件和结论声明让 AI 输出更详细的形式化描述再由人工修正反例搜索耗时太长搜索空间过大或验证器效率不足统计单轮验证耗时观察是否存在大量无效候选加入启发式条件优先检查高概率破坏约束的边界值Lean 环境安装后无法编译例子版本不匹配或依赖缺失查看官方安装说明检查 lean 版本和 editor 插件切换到官方推荐的稳定版本按教程重装这一部分不必期望一次全部解决但至少提供一个排错思路。任何 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 生成候选、让工具做验证、让经验做判断这才是面对这类事件最理性的态度。