AI数学证明如何验证：反例搜索、引理拆分与形式化验证

最近有一个画面感很强的争论在开发者圈子里流传某 AI 模型花了一整晚“证明”了一个重要数学猜想数学家们只用了 24 小时就把结果驳回。驳回理由并不是“你在第 87 行算错了”而是一句更耐人寻味的话AI 的证明里每一句话都是对的但它跟原猜想已经没有任何关系了。这个场景是否来自真实新闻其实不重要。重要的是它精准地命中了当前大模型处理数学问题时的核心软肋大模型非常擅长生成“单独看都正确”的句子却很难组织一个“整体上站得住”的证明。这篇文章不会去吹捧或贬低任何一家模型厂商也不会把 AI 数学能力一棍子打死。我要做的是三件事第一拆解为什么会出现“逐句正确、整体无关”的证明第二给出一套可以在本地运行的验证方法包括反例搜索、引理拆分和形式化验证第三整理一个适合工程师和研究者的 AI 数学证明工作流让你以后再看到 AI 输出的长篇证明时不会轻易被“流利感”带偏。如果你是做算法、安全、编译、AI 应用或者任何需要严谨推理的开发工作这篇文章的判断框架同样适用。1. 从一场“被驳回的证明”说起先把这个场景还原得更具体一点。假设你给 AI 一个数论猜想每个正整数都可以表示为两个整数的平方和。AI 在几分钟内生成了一份十几页的证明。它先定义了整数、完全平方数、模运算然后引用了若干“标准定理”最后用一段看起来很有力的推导收尾声称猜想得证。数学家拿到这份证明后并没有真的逐行去检查每一处计算。他们先做了一件事看证明的整体骨架能不能覆盖目标命题。结果发现这份证明里很多独立引理单独拿出来都是真的AI 证明中的句子是否成立在证明中的角色如果整数 n 模 4 余 3则 n 不能表示为两个平方数之和成立这是在描述一个“否证”条件存在无穷多个整数可以表示为两个平方数之和成立这是在说明这个集合很大上述两个事实结合即可证明每个正整数都能表示为两个平方数之和不成立这是最关键的逻辑跳跃前两句单独看都没有问题。一个熟悉的读者甚至会觉得 AI“懂数学”。但从第一句到第二句再到最终结论中间根本不存在有效的推导关系。换句话说AI 证明了若干个它自己找来的小定理但这些小定理组合起来并没有触及目标命题。数学家为什么能在 24 小时内驳回因为判断一个证明是否成立很多时候不需要逐字审计只需要检查证明的“逻辑依赖图”结论是否真的从前提一步一步长出来。如果中途断掉了后面的内容再漂亮也没有意义。这个小例子是教学意义上的简化但它是理解 AI 数学短板的最好入口。接下来我们需要回答一个更根本的问题为什么大模型会犯这种错误2. 为什么 LLM 的数学推理是“局部正确”模型要理解这种“局部正确、整体无关”必须先理解大模型的生成机制。大模型的核心训练目标很简单给定前文预测下一个最合适的 token。它学到的不是“逻辑规则”而是“文本序列的概率分布”。在数学文本的语料上训练后模型确实学到了大量数学表达方式包括定义、定理、证明词汇、推导句式甚至能模仿出很标准的论文气口。但数学证明从来不是一个“逐句预测”的问题。一个真正的证明尤其是复杂猜想需要满足长距离约束你在第 2 页引入的变量可能要在第 20 页被正确使用你在前面假设的条件必须在整个证明过程中保持不变你的最终结论必须和被证明的命题逐字对应。这些约束跨越的 token 数量往往成千上万而大模型的注意力机制虽然能捕捉长程依赖却无法保证一条完整的、经过推理规则校验的“逻辑链”始终不漂移。我比较喜欢用实习生来类比这件事。一个读过大量数学论文的实习生可以非常流畅地写出一段“看上去很专业”的文献综述甚至每一句引文都是真的。但如果你让他独立完成一篇完整证明他可能会犯三种典型错误结论漂移写着写着目标命题被悄悄替换成了另一个更简单、更容易证明的命题。每句话都合理但题目已经从“证明 A”变成了“证明 B”。伪引理模型构造了一个中间引理这个引理本身可能是对的但它和最终结论之间没有可验证的推理步骤。循环论证在长文本中前面用了后面的结论后面又引用前面的结论人工读者很难在一遍阅读中察觉。这三种错误有一个共同点模型自己无法发现它们。原因在于大模型没有“独立于生成过程的验证器”。它生成下一句话的时候依据的是语义相似性和文本惯性并不是一个能像数学内核检查器那样判断“这一步能否从前提推出”的机器。所以模型输出“证明完成”时它表达的并不是“我验证过”而是“根据文本模式这里应该出现一句收尾的话”。这就是我们经常看到的场景AI 证明的流畅度和正确性没有直接关系。真正的数学正确性必须靠外部工具或者人来约束。3. 数学证明为什么是“整体结构”问题现在需要把“整体性”这个词讲得更技术一点。如果把证明可视化它其实不是一行行文字的线性排列而是一棵推理树。树根是最终要被证明的目标命题树叶是公理和已知定义树枝是每一步推理规则。从树叶到树根必须存在一条从假设到结论的完整路径任何一个节点缺失整棵树就无法成立。形式化方法里管这种约束叫proof obligation也就是“证明义务”。意思是推理链中每一个节点都承担着一个义务你必须证明“从这个前提出发按照这条规则确实能得到这个结论”。不是一个模糊的“显然”而是可检查的规则应用。我们用前面那个例子再来一次。目标命题 P每个正整数都能表示为两个平方数之和。AI 证明了引理 A若 n 模 4 余 3则 n 不能表示为两个平方数之和。引理 B存在无穷多个正整数可以表示为两个平方数之和。现在问题来了从 A 和 B 出发能得到 P 吗不能。A 说的是“有些数不可能表示”B 说的是“有些数可能表示”。这两件事合在一起甚至只能得出“有些数能表示、有些数不能表示”的结论反而否定了 P。但 AI 在文本上做了一个看似合理的收尾“综上所述猜想成立。”这个收尾就是一次典型的证明义务违约。这个结构和软件工程里的一个常见问题很像每个模块的单测都通过不代表整个系统满足最终需求。更隐蔽的是模块本身是真的、代码也确实跑通了但架构设计根本就没覆盖用户要的那个场景。AI 数学证明的失败很多时候正是这种“架构级失败”而不是“编码级失败”。所以当你看到一份 AI 生成的长证明时第一件事不是去检查它的第 42 行有没有算错而是先问这份证明的推理树真的长到了目标命题上吗4. 第一步验证用反例搜索检验 AI 证明的结论聊到这里我们应该从“分析现象”切换到“动手验证”。面对 AI 生成的数学结论最有效的第一步验证永远不是去读证明而是先检查结论本身是否可能是假的。很多数学猜想是普适陈述只要在某个小数值上不成立整个证明就直接失效。这种检查在本地几秒钟就能完成成本极低、收益极大。环境要求很低Python 3.8 及以上版本使用标准库math即可不需要额外安装第三方依赖。下面我们用“每个正整数都能表示为两个平方数之和”这个伪猜想来做一次反例搜索。# 文件路径counter_example.py import math def can_be_sum_of_two_squares(n: int) - bool: 判断 n 是否可以表示为两个整数的平方和 limit math.isqrt(n) for a in range(limit 1): b2 n - a * a b math.isqrt(b2) if b * b b2: return True return False counter_examples [] for n in range(1, 101): if not can_be_sum_of_two_squares(n): counter_examples.append(n) print(counter_examples[:20])运行这段脚本输出会包含一批反例[3, 6, 7, 11, 12, 14, 15, 19, ...]也就是说仅仅测试前 100 个正整数就已经能证明“每个正整数都能表示为两个平方数之和”是假的。既然目标命题本身是假的AI 给出的任何“完整证明”都必然是无效的。这个看似简单的操作在真实工作里非常有价值。AI 生成的结论经常是“看起来普适”但反例搜索往往在最开始就能拦截掉一批错误。反例搜索不能证明结论为真但它能非常高效地证明结论为假。把它放在整个验证流程的第一层性价比极高。如果你面对的不是数论问题而是算法问题同样可以把输入空间缩小后做暴力枚举检查 AI 输出的算法是否真的满足约束条件。这个思路是通用的。5. 第二步验证局部引理可以是真的证明依然无效反例搜索能拦截掉“结论为假”的证明但还不能解决数学家的那个难题如果结论恰好是真的或者反例搜索找不到反例怎么办这时候AI 证明里的局部引理可能是对的但推理链仍然是断裂的。我们用同一个例子来演示。虽然“每个正整数都能表示为两个平方数之和”是假的但 AI 证明里引用的引理 A 却是真的引理 A如果整数 n 模 4 余 3那么 n 不能表示为两个平方数之和。这个引理为什么真因为完全平方数模 4 的结果只能是 0 或 1两个平方数之和模 4 的结果只能是 0、1、2永远不可能是 3。所以 n 模 4 余 3 时确实不存在分解。我们可以先单独验证这个引理在小数值范围上是成立的# 文件路径verify_lemma.py import math def can_be_sum_of_two_squares(n: int) - bool: limit math.isqrt(n) for a in range(limit 1): b2 n - a * a b math.isqrt(b2) if b * b b2: return True return False def lemma_a(limit: int) - bool: 检查引理 An 模 4 余 3 时n 不能表示为两个平方数之和 for n in range(1, limit 1): if n % 4 3 and can_be_sum_of_two_squares(n): return False return True print(lemma_a(10000))输出结果True对前一万个正整数引理 A 确实是成立的。换句话说AI 证明里引用的这个局部结论不是编造的它经得起数值检验。同时我们再用第 4 节的脚本检查目标命题又会立刻得到反例。这个组合非常有意思AI 说了一个真的引理也引用了一个真的例子但它从一个真引理推导出一个假结论。说明断裂点发生在引理和结论之间的推导关系上而不是发生在单个引理的内容上。在代码世界里这相当于每个函数都通过了自己的单元测试但整个系统组合起来根本不满足需求。你不可能通过把单元测试跑得更多来发现这种架构级错误必须去做“连接检查”引理 A 到底是如何被用来推出结论 P 的如果 AI 只是把它们放在同一篇文章里那就不算证明。所以第二步验证的关键是把 AI 证明拆解成若干引理不仅检查每个引理是否为真还要检查每个引理和目标结论之间是否存在真正的推导链。这一步是人工审查的核心工作也是 AI 最容易作弊的地方。6. 第三步验证用 Lean 让 AI 无法“跳步”前两步验证仍然依赖人的判断。那么有没有办法让机器来强制检查“推导链”是否完整有这就是形式化证明系统。目前比较主流的形式化证明工具包括 Lean、Coq 和 Isabelle。这里以Lean 4为例。它的核心思想是你把证明写成代码交给一个极小的、可信的内核去检查。每一个推理步骤都必须落到固定的推理规则上不允许任何“显然”“由此可得”“综上所述”。在 Lean 中未完成的证明可以暂时使用sorry占位但任何带有sorry的定义都会被认为是依赖未完成假设的内核会记录一个名为sorryAx的依赖。这意味着AI 生成的文本证明再长、再流畅只要不能转换成 Lean 的合法证明项就无法通过检查。下面是一个示意性的 Lean 代码展示我们前面讨论的目标命题和局部引理-- 文件路径ProofSketch.lean import Mathlib /- 这是 AI 声称已经证明的目标命题 每个正整数 n 都可以表示为两个平方数之和。 这个命题实际上是假的。 -/ theorem ai_claimed_theorem : ∀ n : ℕ, n 0 → ∃ a b : ℕ, a * a b * b n : by -- 这个目标无法完成。如果你尝试在 Lean 中证明它 -- 会发现自己卡在一个无解的证明义务上。 sorry /- 这是 AI 证明中引用到的局部引理 如果 n 模 4 余 3那么 n 不能表示为两个平方数之和。 这个引理是真空的仍然需要完整证明。 -/ theorem lemma_a (n : ℕ) (h : n % 4 3) : ¬ (∃ a b : ℕ, a * a b * b n) : by -- 这里可以继续展开模运算证明但先留作占位 sorry这里并不是一份完整代码但它说明了关键机制Lean 会明确告诉你在哪个地方卡住了哪个证明义务没有被完成。如果你使用#print axioms lemma_a查看依赖会看到sorryAx这表示这个“证明”实际上并不算数。在实际的 AI 数学研究里现在更受关注的路径并不是让 AI 直接生成自然语言证明而是让 AI 生成 Lean tactic 序列再由 Lean 内核去验证每一步是否合法。模型负责提出思路和尝试策略内核负责裁决。这套机制最大的价值就是AI 无法再用“流畅的废话”来伪装证明因为它无法骗过类型检查器。当然形式化证明的代价也很高。把一篇十几页的数学证明完全形式化往往需要几周甚至几个月的工作量。但在高风险领域比如核心密码学算法、编译优化、共识协议正确性证明这个代价是值得的。7. 把 AI 证明纳入可信工作流四层验证法如果你希望在自己的项目里使用 AI 辅助数学推理或算法验证不建议直接拿 AI 的最终输出当结论。更稳妥的方式是建立一套分层验证流程每一层都有明确的可执行检查。第一层结论层反例搜索。拿到 AI 输出的普适结论后先在目标域内做小规模枚举寻找反例。数字是几万还是几十万取决于你的算力但量级不能太小。如果发现反例直接驳回不需要再读证明。第二层引理层拆分与独立验证。把 AI 证明拆成若干个独立的中间结论逐个用数值实验、符号计算或人工推导验证。这一步能拦截掉“模型编造引理”的情况但要注意引理全对推导仍然可能断裂。第三层推导层逻辑连接审查。对每个引理检查它和目标结论之间的关系这个引理是在什么条件下成立的结论需要什么条件两者是否匹配如果 AI 只是把几个真命题放在一篇文章里却没有展示从它们到结论的规则应用这就是断链。第四层形式化层核心路径用 Lean 或 Coq 验证。对最终要作为结论使用的证明至少要选择一条从关键假设到结论的核心路径做形式化验证。这一步成本高但它是当前唯一能自动防止“整体无关”的手段。在实际操作中可以把上述流程固化成一个 AI 审查提示词让模型先自我检查一次。但你必须清楚提示词并不能保证模型一定会执行它只是把审查步骤明确化。请按以下步骤审查我给出的数学证明不要生成新的证明 1. 提取目标命题 P并判断全文结论是否与 P 完全一致。 2. 将证明拆解为关键引理列表 L1, L2, ...。 3. 对每个引理注明它是已知定理、推导结果、还是未经证明的假设。 4. 判断是否存在一条从引理到 P 的完整推导链。 5. 如果存在逻辑跳跃指出发生跳步的是第几步。 6. 不要修改证明内容只输出审查结论。这套四层流程的核心思想并不复杂永远把 AI 当成假设生成器而不是证明裁决者。模型负责提出思路、写草稿、尝试不同的推理路径最终结论必须经过可重复的外部验证。8. 常见误区与排查思路在验证 AI 数学证明的过程中有几个误区非常普遍尤其是第一次接触这个问题的开发者容易踩中。现象潜在风险排查方式正确姿势模型说“证明完成”模型没有自我验证能力只是模仿了收尾句式查看最终结论是否精确等于目标命题强制要求输出可验证的证明项而不是一句收尾证明中的每个局部引理都能通过数值验证局部为真不代表整体可推导检查每个引理到结论的推导规则做推导链审查而不是重复数值验证证明非常长、引用大量定理长度和术语密度会掩盖逻辑跳跃画出证明骨架标注每个引理的用途先看结构再读细节数值实验覆盖了大量样本覆盖样本再多也不能证明无穷域明确区分验证和证明用反例搜索证伪用形式化证明证实模型引用了某个著名定理可能只借用了定理名字没有检查适用条件翻回原文核对定理使用条件对关键定理做展开检查模型拒绝承认错误AI 不具备立场只是在生成更顺滑的文本提供具体反例或指出断链位置以反例和形式化结果为准其中最容易踩中的误区是把“数值实验通过”当作“命题为真”。这是数学和软件工程里最经典的混淆测试可以证明存在 bug但不能证明不存在 bug。AI 生成证明时经常覆盖到几千、几万个样例看起来很有说服力但只要有一个反例整个证明就不成立。另一个容易被忽视的问题是AI 可能反复引用一个并不存在的定理或者把已知定理的适用条件悄悄改掉。如果你对某个领域不熟悉很难一眼识别。这正是为什么专家审核和形式化验证仍然不可替代。9. 工程化建议与总结把 AI 数学证明的验证引入工程实践时有几个建议可以直接落地。第一把证明当作代码来管理。AI 生成的证明草稿、反例搜索脚本、Lean 证明文件都应该纳入版本控制器。你无法信任一个无法复现的“证明”但你完全信任一段可以在 CI 里自动运行的验证脚本。第二在团队里明确分工AI 负责生成候选证明和反例猜想工程师负责搭验证流水线数学家或领域专家负责最终逻辑审查。如果没有领域专家至少要保证有人能读懂证明骨架而不是只读结论。第三对不同风险采用不同验证深度。内部实验、教学演示、思路探索阶段反例搜索加引理拆分就够用了而一旦涉及安全关键系统、核心算法正确性、密码学协议这类场景必须走到形式化验证层。回到开头那个场景AI 用一晚上写出几十页“每句话都是对的”证明数学家 24 小时驳回不是因为他们更聪明而是因为他们知道一件事——证明的价值不在于每一句话是否漂亮而在于从假设到结论的那条路是否真正走通了。对你我这样的工程师来说这也是最好的提醒。AI 生成的代码、注释、架构设计、算法证明都只是“候选答案”。真正的可信度永远取决于我们是否能在它周围建立一套独立于模型生成过程的验证机制。反例搜索、引理拆分、推导审查、形式化验证这套组合拳越早接入你的工作流你就越不会被“流利但无关”的证明带偏。下次再看到 AI 生成的长篇证明先别急着转发问四个问题目标命题被精确证明了吗反例搜索做了吗关键引理和结论之间的推导链完整吗核心结论有没有通过形式化检查这四个问题问完很多看似惊艳的证明会自然褪色而真正有价值的证明则会更加显眼。