据《新科学家》报道,OpenAI 在一项与纳维-斯托克斯方程相关的证明工作中,把数学内容错误地翻译成了代码。也就是说,问题并非出在证明思路本身是否成立,而是出在从数学表述到机器可检验代码的这一步转写上。目前公开信息有限,具体错在何处、影响范围多大,尚不清楚。
纳维-斯托克斯方程描述流体运动,其三维光滑解是否始终存在、是否可能发生爆破,是克雷数学研究所悬赏的千禧年大奖难题之一,被普遍视为数学与物理交叉领域最难的问题之一。近两年,AI 系统开始被用于寻找证明思路、生成形式化证明或在证明助手中补全引理,这一方向因此受到高度关注。
这条消息的重要性在于它指出了这类工作链条中最容易被忽视的一环。把数学翻译成代码,涉及量词顺序、边界条件、函数定义域、极限与收敛性的精确含义等大量细节,任何一处偏差都可能让代码通过检查,却对应到另一个命题——甚至是一个更弱或已被平凡成立的命题。形式上“机器验证通过”,并不等于数学上真的证明了想证的东西。
对 AI 做数学的评估而言,这意味着不能只看代码是否跑通,还需要人工核对代码与原始数学陈述之间的语义对应关系。若转写环节由模型自动完成,这类偏差尤其难以被外部察觉。相关工作的可信度,很大程度上取决于是否公开完整的形式化脚本与逐步的对应说明,供同行独立复核。
在更多细节披露之前,对这整件事更稳妥的态度是:既不把它当作 AI 攻克难题的突破,也不据此断言 AI 做数学不可行,而是把它视为一个提醒——形式化的最后一公里,仍然需要人来把关。
