夜雨聆风
AI能做微积分,却证不了一道初中竞赛题——这个反差藏着什么秘密
AI能做微积分，却证不了一道初中竞赛题——这个反差藏着什么秘密
ChatGPT能在几秒内解出高考数学压轴题，却可能在一道需要「灵光一现」的竞赛证明题上卡壳。这不是算力不够，也不是训练数据太少。这个反差，指向了一个关于「智能本质」的更深问题。
先说一个让很多人困惑的现象。你把一道高中数学题扔给 GPT-4，它大概率能给出步骤清晰的解答。但如果你让它严格证明「存在无穷多个素数」——这道两千年前欧几里得就解决了的题——它给出的「证明」经常在逻辑上有漏洞，或者只是在复述结论，而不是真正在推理。一个能「解题」的系统，却在「证明」上频频失手。这个反差不是偶然的。
解题和证明，是两件完全不同的事
大多数人把「解数学题」和「做数学证明」当成同一件事的难易之分。其实它们是两种根本不同的认知活动。解题是在已知路径上走得快不快的问题——你知道终点在哪，你只需要找到那条路。而证明，是在一个没有地图的空间里，从零构建一条必然成立的逻辑链。终点本身是否存在，你也不确定。
更关键的区别在于：解题可以「差不多对」。你用微积分算出一个近似值，误差在可接受范围内，这个答案就是有效的。但证明没有「差不多」。一个证明要么是严格成立的，要么就是错的——中间没有灰色地带。这对 AI 来说是致命的挑战，因为当前语言模型的核心机制是概率预测，而不是逻辑推演。
语言模型在「说数学」，不是在「做数学」
这里有一个经常被忽视的技术细节。GPT 这类大语言模型，本质上是在预测「下一个 token 最可能是什么」。它见过海量的数学文本，所以它知道在「设 n 为整数」之后，通常接的是什么句式；它知道「反证法」的标准格式是什么样的。它输出的内容，是对数学语言的高度拟真，而不是真正的逻辑运算。
「
AI 写出来的证明，像是一个背熟了所有棋谱却从未理解棋理的人下的棋。
」
这个区别在简单题目上不明显，因为简单证明的「语言模式」和「逻辑结构」高度重合——见过够多例子，拟真就能蒙对。但一旦题目需要真正的创造性跳跃，比如引入一个非显然的辅助构造，或者把两个看似无关的领域联系起来，语言拟真就会原形毕露。它会生成一段「看起来像证明」的文字，但仔细检查，逻辑链条在某处悄悄断了。
数学证明需要什么，AI 恰好缺什么
1形式化验证能力：每一步推导都必须严格符合公理系统，不能靠「直觉上显然」跳过
2搜索与回溯：证明路径往往是死胡同——走错了要退回来换方向，这需要真正的状态追踪
3创造性构造：最难的部分是「想到用什么方法」，这不是从已有模式中检索，而是真正的原创组合
4元认知：知道自己「不知道」，知道某步推导是否真的成立——而不是流畅地输出错误内容
其中最致命的是最后一点。语言模型有一个著名的毛病：它不知道自己在胡说。在数学证明里，这个问题被放大到极致。一个人类数学家如果不确定某步是否成立，他会停下来，标注「此处存疑」，或者换一条路走。但语言模型会非常流畅地继续往下写，把一个有漏洞的前提当作已证结论，最终交出一篇读起来很顺畅、但逻辑上已经塌了的证明。
有没有解法？有，但代价很高
3
当前最主流的三条路线：符号系统、强化学习、混合架构
目前学界在尝试几条路。一是把语言模型和形式化证明系统（比如 Lean、Coq）结合起来——让 AI 生成证明草稿，再由严格的形式化系统来验证每一步是否真的成立。这条路有效，但极其昂贵：把自然语言数学翻译成形式化语言本身就是一个巨大的工程。二是用强化学习让模型在「尝试-失败-回溯」的循环中自我改进，DeepMind 的 AlphaProof 在 2024 年的国际数学奥林匹克上用这个思路解出了几道题，但那是专门训练的系统，不是通用能力。三是混合架构：让语言模型负责「想方向」，让符号引擎负责「验证每步」。这是目前最被看好的路线，但离真正实用还有相当距离。
这里有一个更深的问题值得想一想。数学证明本质上是人类思维的一种极端形式——它要求你在完全没有外部反馈的情况下，纯靠内部逻辑自洽地构建一个结构。这和「根据上下文生成合理文本」在基因层面就不同。当前的 AI 范式，是从「语言」出发去逼近「思维」；而数学证明告诉我们，有些思维活动，也许不能从语言这一侧被还原。
当然，说「AI 做不了数学证明」是一个过于草率的结论。更准确的说法是：AI 目前能做的，是对数学证明的高质量模仿，而不是真正的证明。在大多数实际场景里，这个区别不重要。但在需要绝对严格性的场合——比如验证一个密码学协议是否安全，或者确认一个新定理是否真的成立——这个区别就是一切。
✦ 小结
AI 在数学证明上的局限，不是工程问题，而是范式问题。解题靠模式匹配，证明靠逻辑必然；语言模型擅长前者，而后者要求的「严格自洽」和「知道自己不知道」，恰好是概率预测机制的盲区。这个反差值得我们认真对待——不是为了贬低 AI，而是为了更清醒地理解它到底擅长什么。