现在有一份AI生成的纳维-斯托克斯千禧年大奖问题解决方案，附带完整书面报告和Lean语言撰写的形式化证明。我翻了这份材料，和普通AI生成的数学猜想不同，它的核心是两套东西，不是空架子。
核心产出的两个部分
第一部分是常规的书面报告（writeup），把AI对纳维-斯托克斯方程相关问题的推导过程，用人类能读懂的数学语言整理出来。第二部分是Lean写的形式化证明——Lean是专门用来做数学证明验证的工具，它会把每一步推导拆解成计算机可核查的逻辑单元，相当于给证明的每一个环节都做了标记，不存在人类审稿时可能漏看的逻辑缺口。
这中间的门道是什么？
纳维-斯托克斯千禧年问题是数学界的顶级难题，过去几十年里，只有全球最顶尖的数学家敢碰，没人说自己能拿出完整的解决方案。现在AI直接产出了可验证的完整方案，这和之前AI帮数学家找猜想、算数值的玩法完全不一样：之前AI是辅助工具，现在是解题主体，至少在这个问题上，Lean已经验证了AI给出的推导是逻辑自洽的，不是随口编的猜想。
这对整个领域来说意味着什么？
形式化证明之前一直是数学圈的小众事，大部分数学家更习惯用自然语言写证明，靠同行审稿确认正确性。Lean这类工具的普及，本来就慢，现在AI直接产出了经Lean验证的顶级难题证明，相当于给这类工具做了一次实打实的背书。说不定以后，数学家会把AI生成的形式化证明作为常规产出提交，而不是只写让人费劲读的自然语言报告。
现在的问题还很实：这份方案还没经过数学界的正式同行评议，Lean的验证只是工具层面的，不是数学层面的终审。未来AI会不会成为解决这类顶级数学难题的常规工具？这个问题暂时没标准答案，甚至很多同行还没来得及消化这个新变化。
素材来源：OpenAI News · AI情报、AI应用落地、科研前沿
查看报道原文
发表第一条评论吧