头条与内幕：数学、科学与工程中AI的理解与信任
内容提要
OpenAI宣称证明纳维-斯托克斯方程有限时间爆破，引发AI在数学中作用的讨论。作者认为，证明不仅需正确，更需增进理解。在气候预测、飞机设计等领域，预测须先于验证被信任，因此需可审计的因果链。应将AI嵌入物理守恒律等可审计框架，用于学习可单独检验的闭合模型，而非端到端黑箱，从而让理解与预测相互促进。
延伸解读
AI证明的局限：正确性不等于理解
OpenAI用约1万个AI代理探索并形式化验证了纳维-斯托克斯方程有限时间爆破的证明，但作者强调，证明不仅需正确，更需增进对数学结构的理解。正如Yehuda Rav所言，定理是头条，证明是内幕。一个正确但无法被数学界消化理解的证明，只给了头条而缺少故事。问题不在于证明者是人还是机器，而在于推理是否推进了集体理解。
预测需先于验证被信任的领域
在气候预测和飞机设计等领域，预测必须在被经验验证之前就获得信任，因为验证太慢、太贵或太危险。例如，飞机只有造好才能试飞，而极端降雨预测要指导当下建设的基础设施，却可能数十年后才受检验。此时，从假设和输入数据到预测结果的可审计因果链是信任的关键，这约束了AI的使用方式，不能依赖端到端黑箱。
端到端AI模型在气候投影中的缺陷
端到端AI天气模型每日可验证，适合短期预报，但用于气候投影则有问题：它没有温室气体浓度影响天气演化的路径，通常不将浓度作为输入，即使输入也无观测可学；且不强制能量等守恒律，长积分会漂移。因此，目前不能信任它投影未观测过的温室气体浓度变化下数十年的气候响应。
可审计框架：将AI嵌入物理守恒律
作者建议将AI嵌入可审计的脚手架，如物理守恒律，用数值方法以受控误差求解大尺度，同时从数据学习未解析小尺度的闭合模型。闭合模型需作为解析状态的函数来学习，并可用高分辨率模拟、观测或实验单独检验。AI能加速搜索闭合模型或证明策略，候选通过检验后成为人类研究的新对象，使理解与预测相互促进。
Q&A
OpenAI 宣称证明了纳维-斯托克斯方程有限时间爆破，这个证明是如何被验证的？
该证明由约 10,000 个 AI 智能体并行探索多种方法产生，随后在 Lean 中形式化并验证。形式化验证支持其正确性，但数学家仍在消化它。
为什么说一个正确的证明不一定能增进理解？
证明确定了陈述的真值，但 Terry Tao 等人认为证明的另一部分作用是推进对基本结构的概念性理解。正如 Yehuda Rav 所说：“定理是头条，证明是内幕。”一个正确但无法理解或未被数学界消化的证明，只给了头条而没有内幕。
在气候预测和飞机设计等领域，为什么不能仅靠端到端 AI 模型？
因为这些领域的预测必须在被经验验证之前就被信任，验证太慢、太贵或太危险。端到端 AI 模型缺乏可审计的因果链，不强制守恒律，长期积分可能漂移，且无法表示温室气体影响气候的因果路径。因此需要可审计的因果链，从假设和输入数据到预测结果，各环节有已知的有效性限制并可单独检验。
如何将 AI 嵌入可审计框架来提升预测可信度？
将 AI 嵌入可审计的脚手架中，如物理守恒律。用数值方法以受控误差求解大尺度上的纳维-斯托克斯方程，同时从数据中学习未解析子网格尺度的闭合模型，其中一些普适性假设可辩护且可单独检验。这样脚手架基于已知方程指导外推，而非依赖与当前数据绑定的端到端模型。
AI 在湍流闭合模型搜索中如何应用？
AI 可以加速闭合模型搜索：神经网络闭合模型可单独测试并部分解释；符号回归（如 SINDy）可从字典中选择项来学习更易解释的闭合模型；AI 智能体开始闭环运行闭合搜索，提出符号闭合，用高分辨率模拟、观测或实验测试并修订。成功后闭合模型可审计并事后理解。
AI 在数学和湍流闭合搜索中的使用有何相似之处？
两者都使用验证器进行检查：数学中用 Lean 检查证明，湍流闭合中用高分辨率模拟、观测或实验检查。数学中的检查是完整的，而湍流闭合的检查仅限于所覆盖的条件，因此信任局限于测试过的条件。AI 能加速搜索更大空间，候选通过检查后成为人类研究的新对象，使理解与预测相互促进。
