数学证明被 AI 生成出来不代表数学问题被解决了。最近这个被反复讨论的案例里最值得关注的不是模型有没有“攻破”猜想也不是数学家有没有驳回而是“证明中的每一句都对但整体已经和原猜想无关”。这类失败模式比你直接看到一个错误答案更隐蔽也更值得写下来拆一遍。因为它暴露的是长链条推理中最难控制的问题目标漂移。下面我按这个案例给我的触动把数学证明、AI 验证、形式化工具和日常编程里同样的坑一起说清楚。1. 这个被驳回的证明问题出在“整体目标”而不是“局部推导”1.1 “每句话都对”为什么反而更难排查如果一个 AI 系统给出的证明里有明显的计算错误比如把加法算错、把条件写反人很容易抓住问题。困难的是另一类情况你检查它写的每一句话发现推理规则都用得没问题表达式没有硬伤符号替换也符合语法但读到最后发现它证明的已经不是原来那个猜想。这种状态下AI 没有“撒谎”也没有“胡编”它只是在推理过程中悄悄换掉了目标。我理解数学家在 24 小时内驳回这个证明不是因为开了什么特殊外挂而是因为他大概率没有从头到尾逐行读。他先做了两件事第一看结论是否完整复述了原猜想第二找证明中间是否引入了原猜想没有的新条件。这两步一旦发现偏差后面根本不需要继续检查细节。这和代码 review 非常像。一个函数内部写得再漂亮如果调用它的业务逻辑理解错误最后的整体行为就是错误的。逐行正确只能证明这段代码没有语法问题和明显的逻辑矛盾不能证明它完成了需求。1.2 从“命题证明”到“证明走样”问题通常发生在规划层数学证明可以粗略分成两个层次推导层每一步用什么公理、定理、等价变换。规划层整个证明的骨架是不是围绕主命题展开关键引理是否都指向最终结论。LLM 生成证明时推导层往往表现不错因为它在大量数学文本上训练过熟悉常见的推理模式和符号操作。但规划层是另一回事。模型需要先在心里形成一个“证明地图”知道从哪个定义出发、经过哪些中间结论、最后如何回到原命题。只要某个中间环节把条件稍微改窄或者改宽后续每一步都可以继续正确但终点已经变了。这种“证明走样”很难通过放大模型规模直接解决。因为它不是某个知识点的缺失而是长序列推理中的目标对齐问题。1.3 数学家的快速驳回依赖一种“专家直觉”有人可能会想既然 AI 的证明每句话都正确数学家 24 小时就驳回是不是太快了其实这不快。专家在判断一个证明是否值得细读时有自己的一套快速筛查方法结论表述是否与原猜想一致是否把“充分条件”悄悄当成了“充要条件”是否引入了原问题没有要求的强条件关键步骤的证明是否过度依赖一个未经验证的大引理是否用新定义替换了原问题中的旧定义只要其中一条有明显嫌疑就可以先整体标记为“无效证明”再根据具体原因考虑是修改还是丢弃。这种专家直觉不是玄学而是长期阅读证明、构造反例、对比不同推导路径之后形成的模式识别能力。对普通开发者来说对应的是“拿到一段 AI 生成代码后先看主流程是否能覆盖核心需求而不是先看每个工具函数写得好不好”。2. 为什么 AI 生成的长链条证明容易与原猜想脱节2.1 单步正确不意味着序列正确在数学里每一步推导如果符合逻辑规则局部看确实是对的。但证明是序列性的前一步引入的假设会传递到后一步。问题往往就出现在传递过程中。一个典型场景是条件替换。原猜想说“对所有满足条件 A 的对象性质 B 成立”。AI 在某个中间步骤把条件 A 替换成了更强的条件 A。它随后证明了“对所有满足条件 A 的对象性质 B 成立”。此时只要每一步都从 A 出发后面的推导当然可以保持正确。但 A 比 A 更窄所以这个结果覆盖不了所有原问题中的对象。从局部看每一步都有道理。从整体看证明已经完全偏离轨道。更麻烦的是如果 A 和 A 看起来非常接近普通读者很难发现替换发生在哪个位置。2.2 LLM 生成证明时的几个典型风险我在实际使用大模型处理逻辑任务时遇到过几类反复出现的风险关键定义偷换。模型在长文本生成过程中可能会把某个术语从“有限集合”悄悄写成“有限子集”后续论证建立在这个更窄的集合上。隐藏的循环论证。证明过程中某个看起来是“引理”的结论其实已经依赖了最终要证明的命题。单看这句话没问题放在整体里就是循环。过度依赖强引理。模型为了推进主线会引入一个非常大的定理。如果这个定理本身等价于原问题这个证明就没有提供新信息只是在绕圈子。分类讨论漏项。证明分成了很多情况每个分支的推导可能都对但所有分支加起来没有覆盖原命题的全部条件。抽象层级失控。模型不断引入新的抽象定义最后证明的对象已经不再对应原始数学结构。这些风险都不适合用“单步校验”来发现。所以只让 AI 生成一个很长的证明然后让人类逐句验证成本高且效果差。更合理的方式是让 AI 先生成证明提纲再由人检查提纲和主命题的关系。2.3 数学家为什么能在 24 小时内驳回快速驳回的关键在于专家不需要验证整座大厦的每一块砖他只需要发现地基位置画错了。这个案例中驳回的关键不是“看得快”而是“知道该往哪儿看”。长期做数学研究的人会积累一个“问题锚点”。拿到一个证明他心里始终清楚原始猜想长什么样。不管中间过程多复杂最后必须回到这个锚点上。只要证明过程中出现了一个偏离锚点的实质跳跃无论后续多流畅整个证明就要被贴上有害标签。这个思路对普通人也适用。你让 AI 帮你写一段复杂脚本时不应该只看代码能不能跑而要把“最初的业务目标”写在旁边每完成一个阶段就回头比对一次这个函数还在服务原本的需求吗3. AI 辅助数学研究时应该用什么标准验收3.1 先定“原始命题锚点”任何 AI 证明输出第一件事不是读内容而是把原始命题单独摘出来。要确保摘出来的这个命题和 AI 最后证明的结论完全一致。具体可以检查三处条件部分是全称还是存在是有限还是无限是任意还是特定。结论部分是存在某个对象还是对所有对象都成立。术语含义有没有在证明中途重新定义关键词。我建议把原始命题写成一个独立块和 AI 输出放在同一页面。这样你比对时不需要来回切页面也不容易因为上下文太长而忘记原始目标。3.2 证明结构审计清单拿到 AI 生成的证明后我一般会按这个顺序做结构审计列出证明中的主要节点。直接看小节标题或关键词例如“定义”“引理”“定理”“证明”。检查每个节点是否由前一个节点自然推出。这个“自然”不是直觉判断而是看推理方向是否一致。找出证明中所有引理确认它们之间没有相互依赖成环。确认每个引理都在主命题路径上至少不出现一个与主命题完全无关的长分支。确认最终结论的措辞确实回到了原始命题而不是回到一个看起来很像的变体。只需要完成这五步很多目标漂移问题就会暴露出来。如果这五步没问题再进入细节逐行验证。3.3 自动验证工具能做什么不能做什么现在有 Lean、Coq、Isabelle 这类形式化验证工具可以检查证明中的每一步是否符合规则。它们能解决“这一步对不对”的问题但不能解决“这个证明是否还在证明原猜想”的问题。原因很简单形式化验证要求你把原始命题也形式化到工具里。如果形式化这一步就把命题翻译错了或者把新定义当成旧定义使用工具只能保证后续逻辑一致无法知道你的输入偏离了人类意图。所以在使用形式化工具验收 AI 证明时最关键的一步是人工检查“被形式化的命题”和“自然语言原始命题”是否等价。这一步没有自动化替代方案。工具越强越容易给人一种“机器已经验证过了”的安全感但这种安全感往往来自对工具边界的误判。4. 一套可复现的 AI 数学证明复核流程4.1 准备阶段记录问题边界在开始复核之前把原猜想的边界条件写清楚。包括所有前提条件所有量词涉及的数学结构不能用哪些高级定理来直接等价替代这些信息不仅是给 AI 看的也是给后续复核者看的。问题边界写清楚了后续验证才有基准。4.2 拆分阶段把 AI 输出拆成可验证的最小单元不要一次性阅读一份 20 页的证明。先让 AI 把证明结构拆成块例如准备工具与定义核心引理 1 及其证明核心引理 2 及其证明主定理的最终推导结论拆分之后重点看块与块之间的衔接而不是块内部细节。如果一个引理和主定理之间没有清晰的箭头关系这个引理再正确对这个证明也没有贡献。在拆的过程里如果发现存在两个核心引理互相引用就需要特别警惕循环。你可以尝试把其中一个引理的证明禁用看另一个是否还能成立。如果不行说明它们是在互相支撑而不是在向主命题推进。4.3 复核阶段每一步都要回答“这跟主命题有什么关系”复核不只是检查错没错还要检查“这段内容为什么存在”。我会给 AI 输出里的每个段落加一个小标注推进主线支撑某个引理解释背景无关内容如果“无关内容”占比过高整个证明就需要降级处理。如果某个很长的分支只是为了证明一个最终没有用到的引理那它多半是目标漂移的产物。判断标准就三条这个结果有没有被后续步骤引用这个结果有没有减轻主命题的证明难度这个结果是不是原命题的推论三条都不满足就不是证明的一部分。4.4 回归阶段用反例和边界条件压测好的证明不只是“从 A 推出 B”还要说明为什么反例不存在。复核时最有效的方法是主动构造边界例子。假设原命题是“所有满足条件 P 的对象都满足 Q”你可以构造一个只满足 P 但不满足任何额外条件的对象看证明过程是否覆盖它。另一种做法是找一个不满足 Q 的对象反向追踪证明在哪一步失效。如果能定位到具体步骤说明这个证明原本是脆弱的如果追踪失败那很可能证明里已经偷偷引入了额外条件。对于数学类任务边界条件就是最好的回归测试。你可以把这个思路理解成给代码写边界测试不是验证正常路径而是制造极端输入看程序会不会崩溃。一个能通过极端样例的证明可信度会显著增加。5. 同样的目标漂移问题在 AI 编程中更常见5.1 用 Codex 等 AI 编程工具时代码可能“每行都对整体没实现需求”AI 生成数学证明和 AI 生成代码底层逻辑非常相似。代码也是长链条结构每个函数、每个判断、每个循环单独看都能编译。但组合起来可能没有实现业务需求。OpenAI Codex 这类项目把 AI 编程工具变成了一个可复现的工程系统它的价值不只是生成代码而是把任务拆解、执行、验证、错误修复做成完整流程。但我看这类工具时会额外关注一个点它如何判定“任务完成”。如果系统只是“代码跑完没报错”那它和 AI 证明里的“每句话都对”是同一个问题。代码能跑不代表它完成了用户描述的业务目标。真实场景里最常见的失败模式是这样的你让 AI 写一个“批量处理文件并输出结果”的脚本AI 生成了很长的代码每个函数都能运行文件也生成了但输出格式和业务要求不一致。步骤都对需求漂了。5.2 用测试和契约把“问题漂移”挡在外面在编程里防止目标漂移的核心手段是测试和接口契约。你的需求必须被翻译成可执行断言这样代码行为是否符合需求才不是主观判断。同一个思路可以带回到 AI 证明复核里把“原始命题”当成接口契约把“证明结论”当成返回值把“关键引理”当成内部函数把“边界条件测试”当成单元测试如果结论没有拼写为契约就算内部实现很漂亮也应该判失败。对普通开发者来说用好 Codex 或类似工具时不要一上来就让它写完整项目。更好的方式是拆成小任务每个任务都有明确的输入输出定义。这样即使某个子任务发生漂移影响范围也是可控的。5.3 从数学证明到软件任务一套通用的审查习惯我喜欢把这套审查习惯称为“目标回归检查”。不管对象是证明还是代码核心动作都是定期回到原始问题上。具体可以这样做开头写下原始问题的一句话版。每次中途生成结果后把当前版本和原始问题对比。一旦发现“当前做的东西已经无法回答原始问题”立即停下来。不要因为前面的步骤已经花了很多时间而不舍得推翻重来。优先保住核心路径然后再补充边缘细节。这套习惯尤其适合 AI Agent 和长任务自动化。不管 agent 是写代码、做纪要、还是生成实验报告单步质量往往不是最大瓶颈整体是否忠于用户需求才是。6. 我对这类案例的几个实操判断6.1 AI 做配角人做主语这个案例给我的第一个判断是AI 可以成为一个很擅长推演的配角但每一个最终结论的主语仍然应该是人。这不是对 AI 的不信任而是对目标定义权的保留。一件事的目标由谁定义最终就由谁负责校验。AI 可以把繁琐的推导过程加速完成但它不能替人类回答“这个问题到底在问什么”。所以我会把 AI 生成的数学证明当作“草稿”来对待而不是“审稿人”来对待。草稿的价值是提供候选路径审稿的价值是判断路径是否通向正确终点。如果一开始就把草稿当成品别人 24 小时驳回你其实已经算快的。6.2 日志和审计是底线AI 生成的长证明和 AI 生成的代码一样必须有过程日志。日志至少要回答三个问题这个结果是怎么来的中间用了哪些大引理中间替换过哪些定义或条件有了日志复核者才能快速定位目标漂移发生在哪一步。没有日志整个证明就是黑盒只能从头到尾重看一遍效率非常低。我把这个要求同样放在 AI 编程工具上。不管用 Codex 还是其他 agent都应该保留每次执行的输入、输出、失败信息而不是只保留最终结果。审计能力不是生产环境才需要的奢侈品而是验证 AI 输出的基本条件。6.3 警惕“正确感”带来的盲区最后一个判断是心理层面的。当 AI 给出的证明每一步看起来都合理时人会自然产生一种“正确感”。这种感觉越强越容易放松对整体目标的关键检查。正确感是目标漂移的催化剂。你要不要尝试读长证明时不急着点头而是每隔几段就问自己一句——“这段内容和我最初想证明的东西还有关系吗”这个问题看起来很简单但它是整篇文章所有操作动作的底层逻辑。数学证明如此AI 编程如此任何长链条任务都是如此。这个案例最值得记住的一点是当 AI 的每一步都正确时依然要保留对整体目标的判断权。这句话对数学、对编程、对后续所有被 AI 辅助的复杂任务都适用。