OpenAI 纳维-斯托克斯相关发布附带 Lean 4 形式化证明

博主 John D. Cook 讨论了将 Lean 4 形式化证明纳入 OpenAI 纳维-斯托克斯相关研究的设想与影响。推演与验证被分别置于生成模型与形式化证明工具的两端。当高深数学分析转变为可逐行核验的代码逻辑，前沿研究的验证壁垒与协作范式也随之出现新的折射。