OpenAI公布719份数学证明 学界指未达形式化标准

OpenAI本周公布719份针对高难度数学问题的解答，并称发布前已咨询一个由顶尖数学家组成的顾问组，以避开上次模型“攻克”长期难题时引发的争议。数学界的回应相当克制，却直指要害：这批成果尚未达到顾问组提出的标准。

这个顾问组名为数学与人工智能顾问组（AGMAI），由普林斯顿高等研究院主持，成员是九位来自世界各地研究机构的知名数学家。9月底，该组织发布了针对前沿实验室的数学研究指南。

指南的第一条要求很直白：停止在闭源模型上测试高难度数学问题。OpenAI的发布说明则写明，它正在用公开研究问题评估自家的闭源模型。

AGMAI在关于这批证明的声明中说，建议被落实了多少，最终要由数学界来评判。面对TechCrunch索取更完整评估的询问，该组织没有回应。

从公开信息看，OpenAI照做了其中一部分，比如尽快公布结果、说明模型如何得出结论。落实情况并不齐整：719份文稿里，只有10份附上了模型的思维链。

数学家们建议，读者难以看懂的论文应当把证明形式化，而OpenAI公布的证明中有42%没有经过这一步。AGMAI还提出，这笔人力账单该由OpenAI来付，因为只有人真正参与，机器产出的答案才可能站得住。

形式化指的是把自然语言写成的证明，翻译成可以逐行编译检查的代码。Lean是数学界常用的定理证明语言，代码通过编译，理论上就说明证明站得住脚。麻烦出在翻译环节。

剑桥大学与伦敦国王学院的数学家本周发布论文，记录了至少两处不一致。纳维-斯托克斯方程描述流体的复杂运动，其完整求解正是悬赏百万美元的千禧年难题之一；OpenAI给出的相关解答里，自然语言证明与背后的Lean代码对不上。

两处出入未必推翻任何一方结论，却指向一个更实际的问题：能不能放心让模型自己把答案形式化，而完全不经过人。论文作者在结论中写道，这类自动形式化的证明不该因为出自模型就被直接信任，它同样要接受同行评议式的审视。

AGMAI原本建议OpenAI附带机器可读的元数据，把自然语言表述与形式化产物对应起来。这次发布中并没有出现这样的元数据。

加州大学洛杉矶分校教授陶哲轩在社交平台上写道，问题被AI解掉之后，提示者往往对数学领域本身没什么兴趣，目标一旦达成便转身离开，也无力就结果答疑、做报告或与同行交流。他是菲尔兹奖得主，长期关注AI与数学的交叉地带。

哈佛大学数学教授Melanie Wood对TechCrunch说，模型被提示解出一道难题、吐出答案的那一刻，并不存在人类的理解，而工作恰恰从那时开始。

数学界的习惯是，人类拿到新结果就要对它负责，通过论文、报告和研讨会让同行把它消化掉。解法被理解之后，其中的策略才能迁移到别的问题上，新知识才有机会落到实际应用里。机器产出的证明如果没人接手，这条链条就断在最前面。

AGMAI要求停止在闭源模型上测试高阶数学问题，理由不难想：数学结论要能被检验，前提是别人能复现过程。闭源模型只交出黑箱答案，同行连追问的入口都不好找。

另一家实验室的路线可以对照。谷歌DeepMind的AlphaProof同样把解答写成Lean代码接受机器检查，在2024年国际数学奥林匹克上解出四道题，接近金牌水平。两家公司对形式化验证的姿态不同，最终会落在数学界愿意花多少时间配合上。

形式化本身是件昂贵的事。把一段证明翻译成代码，常常比想出证明更费工夫，需要受过长期训练的数学家和工程师盯着每一个符号。模型可以批量生成结论，消化它们的成本却要由整个学科来承担。

前沿实验室偏爱发布数量，数字好传播。719份、数百个难题，听起来像一次跨越，而数学界看的始终是每个结论能否被追问、被理解、被接续使用。发布节奏快过验证节奏，留下的就是待清理的账。

我大二那年冬天考数学分析，宿舍暖气不热，桌上摊着一沓从图书馆复印的证明，纸边卷起来，手指冻得握不住笔。我把它们一行行抄进本子，抄完还挺得意，直到考场上老师换了个问法，我一个字也写不出来。抄过和看懂之间，隔着一次补考。现在OpenAI一口气放出719份证明，只有10份附了推理链，剩下的那些我瞄两眼就头大，跟当年那沓复印件没什么两样：看着唬人，追问一句就露馅。我到底从抄写里学会了什么？大概就是别再把抄完当成懂了。

陶哲轩和Melanie Wood说的其实是同一件事：一份证明的价值不在于被生成，而在于被理解。OpenAI这次补上了透明度的一部分，后半程却没有接上。数学界需要的是能站得住的答案，而不是更多的答案。