OpenAI 模型上个月抛出 Navier-Stokes 解失效的反例证明。MIT 工程教育副院长 Justin Solomon 在《Odd Lots》播客里说，他和主持人连第二页都读不下去。这不是八卦，是 AI 数学能力的一次尴尬切片。Navier-Stokes 方程关乎流体运动，解是否永远光滑是千禧年难题。若反例成立，数学界该地震；可读不到第二页，定义、引理、推理链全都没法审。Solomon 不是外行，他读不下去，问题大概率不在智力，而在文本本身。
数学证明不是聊天记录。它需要每一步能被同行复现，或在 Lean 这类形式化工具里逐行检查。AI 擅长生成看似连贯的符号瀑布，但 Navier-Stokes 是非线性偏微分方程，任何一步放缩、一个隐藏假设，都足以让结论从惊天发现变成高维幻觉。若证明无法被人理解，也无法被机器验证，那它更像黑箱里的神谕。OpenAI 模型也许真找到了某种反例结构，但第二页之后可能是循环论证、符号游戏，或模型编出的学术黑话。生成能力与可验证能力之间，隔着一整条推理链。
真正值得追问的是，AI 能否把证明写成人类可检验的样子。如果答案是否定的，再惊人的声明也只能卡在第二页。让模型联手形式化证明助手，也许比追逐头条更接近突破。Navier-Stokes 不是秀肌肉的舞台，而是照妖镜。能生成证明只是一半，能让证明被读懂、被验证、被推翻或接受，才是另一半。
