今天OpenAI 又放了一个大招，用还没有对外的一个内部模型，证明了数百个数学问题。其中包括四维挂谷猜想 (前不久王虹因证明三维挂谷猜想而获得了菲尔兹奖)， 和黎曼猜想的最新成果(所有 Dirichlet L 函数在复平面上 7/8 < Re(s) < 1 的区域里没有零点 。这些虽然还只是宣称，但是有完整的可以验证的证明格式(lean)。这对数学来说，不知道是喜还是优。数学问题的存在其实不是证明本身，是标志人类理性探索进展的标尺。如果数学问题仅仅变成了逻辑证明，而且不是由人来完成的，就无法衔接到我们的知识体系，形成进一步探索的支点。数学不同围棋，虽然AI可以碾压顶级棋手，但是无改围棋作为游戏的乐趣。而AI证明也把数学家和数学文化推到了一个死角。如同辣手摧花，数学界能不能由此紧逼，焕然一新，真的不能那么乐观。