AI解开10道数学难题

8月初，OpenAI放了个大消息：下一代模型Astra，解出了10道悬了多年的数学难题。

注意，不是蒙答案。它写的是完整证明，每道题都能被机器一步一步验证。

10道题里有几道特别硬：

一道是”非sofic群”的首次显式构造。

一道是否定Connes刚性猜想。

都是数学家啃了几十年没啃动的骨头。

验证靠什么？Lean 4，一个能逐步核对证明的系统。AI写完证明，机器验一遍，通过了才算数。证明文件全部公开在GitHub，谁都能去检查。

最扎眼的是成本：OpenAI说，生成这些可验证证明，只花了大约2000美元的算力。

两千美元，解出几代数学家没搞定的题。

换个角度看，这事的重量不在”解出题”，在三个字：可验证。

AI会一本正经胡说八道，大家早见过了。但数学证明这玩意，对就是对、错就是错，机器能严格校验。在”不能说谎”的领域，AI先突破了。

所以别急着喊”数学家要失业”。

更合理的画面是：AI负责天马行空提出想法，人来把关、理解、消化，再往深里走。

从”答你所问”到”做出新东西”，AI这一步，迈得比看起来大。