近两个月来，OpenAI宣称已解决纳维-斯托克斯方程（Navier-Stokes equations，简称N-S方程）相关问题，但数学界对此仍存在广泛争议。截至2023年11月2日，此问题在克雷研究所官网仍未列为“已解决问题”。2023年10月6日，来自伦敦国王学院的应用数学讲师亚历山大·巴斯图尼斯（Alexander Bastounis）、剑桥大学的法比安·奇尔切利（Fabian Circelli）及安德斯·汉森（Anders C. Hansen）在arXiv上发布论文，指出OpenAI所提供的自然语言证明与其对应的Lean形式化证明之间存在显著不一致。这一发现表明，OpenAI公布的计算机验证结果无法直接确认其面对人类读者的数学论文的正确性。

首先，OpenAI在2023年9月8日发布了一份N-S方程存在性与光滑性问题的证明，包含传统自然语言版本和形式化的Lean代码。前者为人类可读的数学叙述，后者则通过Lean语言实现了数学定理的完全形式化，以便使用计算机验证每一步推理的正确性。然而，仅凭Lean形式化的通过并不能说明自然语言证明的正确性，因为计算机验证的适用性依赖于自然语言内容的准确转化。如果在转化过程中改变了数学条件或结论，计算机验证的结果可能与原提议不符。

其次，研究人员发现OpenAI的自然语言证明和Lean形式化证明存在至少两处关键性不一致。第一，证明中的引理8.6要求解级数光滑到m阶，在自然语言证明中要求函数光滑到m+4阶导数，而在Lean形式化中则为m+5阶。后者意味着条件更为宽松，暗示数学判断的严谨性受到削弱。第二，针对引理10.5，Lean形式化版本中所依赖的上界公式引入了新的梯度项AR。研究者认为，这些差异表明，OpenAI的Lean形式化并未逐项验证自然语言论文中的全部证明，而是基于更为宽松的条件开展验证。 千亿球友会

此外，OpenAI针对N-S方程的证明思路也引发了学术界的广泛讨论。N-S方程的核心问题之一在于：流体在三维空间中的运动是否始终保持光滑，或者在某一有限时刻可能发生无穷大的速度，从而产生所谓的“奇点”。OpenAI的模型发现了奇点形成的构造，指出初始静止的流体在光滑外力的影响下，可能形成类似于螺旋的流动状态，随着时间的推移局部速度增大，最终形成奇点，然而流体的整体能量仍然有限。关于该证明相关的讨论中，许多专家认为OpenAI所提出的解与纳维-斯托克斯方程的核心问题并不一致。

综上所述，尽管OpenAI的研究提供了一些有价值的见解，学界对其证明的有效性仍持审慎态度。需要更全面的独立核查以确认该自然语言证明的正确性，同时开发可靠的方法用于数学证明的准确性检验亦显得尤为重要。研究表明，通过适当的形式化方法能够提升证明的严谨性，但在有效性确认过程中仍需对模型及其输出进行严格审视。