看了 OpenAI 这两天在数学上的进展，突然意识到，AI 正在真正彻底改变数学的研究方法。

OpenAI 用了大约 1 万个 AI Agent，连续运行 88 个小时，给出了千禧年难题 Navier–Stokes 方程的一个候选解，并进一步将整套证明转化为了 Lean 形式。

另外，国内也有一个非常重要的数学进展。昨天，南开大学、字节 Seed 和中科院数学所等团队把今年菲尔兹奖相关的三维挂谷猜想完整搬进了 Lean 4。

大家可能还记得，今年菲尔兹奖得主王虹的代表性工作之一，就是解决了困扰数学界几十年的三维挂谷猜想。

这个问题非常难，它研究的是一种看似几乎不占空间，却能包含所有方向线段的特殊集合。过去几十年，数学家一直在尝试理解它背后的结构.....

突然就感觉，AI 正在把数学从一种主要依靠少数数学家长期探索的研究方式，变成一种可以并行探索、快速验证的新型研究方式。

我记得数学家陶哲轩曾经提到过一个很有意思的观点。

在物理、化学、生物这些学科里，提出假设、设计实验、验证结果，本来就是非常常见的研究方式。但数学长期以来有点特殊，它更多依赖理论推导。

数学家当然也会做大量尝试，比如测试不同证明路线，寻找规律，验证一些特殊情况。但这些更多依赖数学家的个人经验和直觉。

比如，我们能不能拿 1000 道数学题，让 AI 分别尝试 20 种不同的证明策略，然后分析哪种方法在哪类问题上更有效。

以前几乎没人能这么做。

AI 的出现，让数学第一次有机会进入到大规模实验数学研究的阶段。其实，刚刚 OpenAI 和字节模型做的事情，本身就在把数学变成一种可以 Scaling 的研究方式。

南开大学公众号提到，这次三维粘性挂谷猜想的形式化工作总共完成了约 180 万行 Lean 代码，其中约 90% 由字节 Seed 团队研发的 Seed Prover 完成。