OpenAI在9月初宣布拿下纳维-斯托克斯方程一个长期悬而未决的问题,和常规的166页人类可读论文一起,还放出了一份Lean 4形式化证明——机器能逐步核验、不容含糊的那种证明。科技评论人John D. Cook按老经验法则算了一笔账:形式化这样一篇论文理论上要132,800人时,OpenAI实际只用了17小时,效率提升了四个数量级。这个对比确实扎眼,但比数字本身更值得盯住的,是它背后一整套还没说清楚的东西:编译通过到底证明了什么,以及——这条时间线本身,是不是站得住脚。
132,800小时和17小时,都不是精确数
Cook的132,800人时,来自2005年数学家Barendregt和Wiedijk提出的经验法则:形式化一页教科书要40个人工小时。他自己又加了一个假设——研究论文比教科书难20倍,166页的论文乘出来就是这个数。这不是实测,是两层假设叠加的估算。
17小时同样需要打个问号。OpenAI这次调用了数百万条agent消息、约1300亿输出token的并行计算,17小时是墙钟时间,不是真实消耗的计算量。把两者直接相除得出"四个数量级",精确算下来其实是约3.9个数量级,离整数四还差一点。这个数字更像一个启发性类比,拿去当基准测试引用就走偏了。
一个月里,这不是孤立事件
把这次公告单独看,容易高估它的意外程度。往前数一个月,类似的动作已经连发了三次:8月1日OpenAI先公布了十项数学与理论计算机科学难题的"进展",每项都附Lean 4证明;9月4日Anthropic宣布用Claude把费马大定理的既有证明翻译成Lean,耗时11天,生成约1300万行代码和29,500个中间定理;9月8日才是这次的纳维-斯托克斯声明。
第一个是新猜想的自动证明,第二个是把已有证明翻译成Lean,第三个又是新构造——三件事性质不同,但被密集地摆在一起,容易让人误以为AI已经在数学研究上全面提速。Kevin Buzzard称Anthropic那次是"非凡的自动形式化成就",这个评价是给"翻译"打分,不是给"新证明"打分,两者不能混着用。
编译通过,不等于数学界认可
Terence Tao在这轮讨论里提了一个区分,比效率数字重要得多:证明检查(proof checking)和陈述检查(statement checking)是两件事。Lean能核验一步推理是否严格遵循逻辑规则,但它不会替你确认——被编码进代码里的那句"定理陈述",在语义上是否真的等于公开宣传的那个结论;也不会自动排查代码库里有没有悄悄引入额外公理。编译通过,只说明代码内部逻辑一致,不说明这份代码忠实翻译了数学家想表达的意思。
编译能过关,公论未必过关
Mathlib社区的反应也不是一片叫好。维护者的顾虑很具体:AI生成代码的速度远超人类审阅速度,即便逐行编译通过,也可能是臃肿、重复、难以维护的产物,社区未来要花大量精力清理,而不是省事。8月18日,Jeremy Avigad、Tao、Ravi Vakil、Akshay Venkatesh等人牵头成立了Palomar Registry,把简短的定理陈述和任意长度的证明分开存档,用Lean加独立内核做双重检验,还要求记录AI使用情况、预算和归属——这套机制解决的是"最低验证标准"和"署名可追溯",但它明确不负责认定新颖性、重要性,或者陈述与原意是否对应。换句话说,连数学界自己人也认为,光靠形式化验证工具,还接不住这波AI证明潮带来的信任问题。
- 风险.纳维-斯托克斯声明发布后,已经有人质疑其工作是否借助了未发表的人类研究成果,署名和研究伦理的争议还没定论。
连时间线本身都对不上
比这些争议更棘手的一点是,关于这一系列公告发生的时间和真实性,目前能查到的说法本身就不一致:一部分资料明确指向openai.com、anthropic.com上具体的公告链接,把它当作已经发生的事件链条来叙述;另一部分资料却提到,截至2026年3月,纳维-斯托克斯仍被视为未解决的千年难题,也没能在OpenAI官网找到对应公告。这两种说法互相矛盾,目前还看不清哪一个更准确。
即便抛开这层不确定,按Clay数学研究所的既定规则,任何千年难题的解答都要在合格期刊发表、经过至少两年等待期,并获得数学界普遍认可,才算正式解决——这意味着不管这次公告本身成立与否,"解决"二字现在都下得太早。对普通读者来说,遇到"AI证明数学难题"这类新闻,更稳妥的态度是先看它是否经过同行评审和时间沉淀,而不是看Lean编译有没有报错。对Mathlib和Palomar Registry这样的机构来说,接下来要看的是能不能把"AI生成的形式化代码"和"数学界认可的证明"这两件事,重新划出一条清楚的界线。