OpenAI 发布了 722 项由 AI 推导的数学成果，数学家们开始追问：功劳该归谁
OpenAI 发布了一批由其内部前沿模型生成的数学成果，公开了一个代码仓库，其中包含许多证明的 Lean 形式化，以及修订与引用方面的协议。此次发布共列出 722 项成果，其中 162 项经过机器校验。
外界的反应，与其说关注这些数学是否正确，不如说关注验证究竟买到了什么，以及这些成果究竟属于谁。
Lean 校验了什么，又没有校验什么
Lean 是一个证明助手。它会依据给定的公理，机械地逐步校验形式化论证的每一步，这意味着一个经过校验的证明不可能存在逻辑漏洞。只要它能编译通过，论证就是从前提中推导出来的。
这是一个很强、同时也很窄的保证。证明助手验证的是形式化陈述能够成立，而不是这个形式化陈述是否表达了随附叙述文字所声称的内容。仍然需要有人逐篇阅读那 162 项经过机器校验的成果，确认 Lean 文件所编码的定理，确实是人们以为的那条定理。形式化本身是一次翻译，而翻译总会走样。
其余 560 项成果则没有这类校验，这意味着这份公开成果集混合了两类证据强度截然不同的结果。说「722 项成果，其中 162 项经验证」比只报一个总数更诚实，但这也意味着标题数字把已验证的那部分夸大了约四点五倍。
功劳归属问题有了新的形态
自数学这门学科存在以来，数学家们就一直在争论功劳如何分配，争论的焦点通常是：谁提出了问题，谁找到了关键一步，谁把它写了出来。AI 生成的成果带来了一种前所未有的版本。
如果模型给出了某个长期悬而未决的公开问题的证明，那么作者是谁？是模型本身吗——可按现行著作权框架，模型也无法成为法律意义上的作者？是向它下提示词的研究者？是整理问题清单的团队？还是训练了这个模型、却不公开其权重的机构？
OpenAI 表示正在推动以负责任的方式发布底层模型。在那之前，社区无法在同一系统上复现这些结果，无法审查训练数据，也无法评估模型的成功是否依赖于训练期间见过相关问题。发表与可复现是两个不同的承诺，而这次发布只兑现了前者。
数学领域还有一个特殊的复杂因素：这个领域的署名靠的是理解。一项证明之所以获得认可，部分取决于它引入了什么思想，而数学思想传播的方式，是人们去读它、发现它有用，并加以拓展。一份没有人完全理解的机器生成证明，无法以这种方式传播。它可以被引用，却很难被在此基础上继续推进。
还有一个现实中的不对称性，将在未来数年内持续给同行评审带来麻烦。一位人类数学家发表了有缺陷的证明，通常会被认为是无心之失，声誉上的后果与错误程度相称。而一个发布 722 项成果、部分正确部分不正确的模型，产出的是一批连对错比例本身都未知的工作，而且没有任何个人会为其中错误的部分负责。期刊的机制并不是为处理这类投稿而建立的：作者身份分散，错误率不是一个事件，而是一个分布。
引用问题随之而来。数学的进展依赖于知道哪些既有结果可以被信赖。一项在 Lean 中经过机器校验的结果是强有力的候选；而一项由模型断言、无人审阅的结果则不是。把这两类结果混在同一次发布里，会让人们更难基于其中任何一类开展工作。
同一天的另一条故事线
OpenAI 的数学发布所出现的这一周里，有若干来自第一方的宣称，却鲜有第三方验证。
Mistral 发布了 Large 4，一个拥有 1 万亿参数的模型，被定位为西方对开源权重中国系统的最强回应。其基准对比被一个回复帖逐行对照 Artificial Analysis 公布的分数进行核查，结果站不住脚——具体而言，是指控它挑选了竞争对手的某个变体来做比较，并错误陈述了一个已公布的第三方数字。
Reflection 发布了 Beam，一个瞄准同一战场的开放权重模型，权重将在本月晚些时候放出。
Anthropic 则扩大了一款用于发现软件漏洞的模型的访问权限，同样附带了自家的第一方数据。
这一周呈现出的模式是：能力宣称到来的速度，快于核查它们的速度。arXiv 面对同一压力的另一种表现形式做出了回应——在 9 月收到创纪录的 40,363 份投稿（是两年前的两倍）之后，将每位投稿人每月的投稿上限设为两篇。
竞争的关键在于让宣称变得可用
关于 AI 与数学的故事，有一种叙事框架是把它当作记分牌：一个模型能解决多少个未解问题。更有用的框架则关注什么能让一项成果被研究共同体所用，而这涉及若干单靠一次模型发布无法提供的东西。
评审人需要理解这一论证。署名需要可追溯。其他研究者需要能在不重新推导的前提下基于该成果继续工作。更广泛的社区则需要有足够的权限访问生成系统，以便自行开展测试。
最后一点正是这次发布的止步之处。一批由他人无法运行的系统产出的成果，更像是一场演示，而非一份贡献。它展示了什么是可能的，却没有交给这个领域任何可以独立据以推进的东西。
这场转变中，困难的并不是数学本身。困难在于，AI 能力如今正超越那些本就为验证它而存在的制度（同行评审、基准复现、署名规范、引用实践），而这些制度运转的节奏是人类的时间尺度。一个模型可以在一次训练中生成 722 项成果。而要弄清其中哪些真正重要、谁应获得认可、它们又带来什么后续，仍然要以年来计量。
还有一种值得说明的对立观点，因为它并非没有道理。一份能编译通过的形式化证明就是证明，无论它由谁、由什么产生。数学一直是以成果本身的价值而非其出处来接受成果的；如果 Lean 验证了一个论证，这个论证就成立。在这种观点看来，署名之争是这个领域应当以常规方式解决的社会学问题，而对可复现性的坚持，等于是要求一种人类数学家从来无需提供的访问权限。没有人会要求一位人类作者公开自己的思考过程。
反驳意见是：人类作者是可以被要求解释其工作的，而解释正是理解所在之处。一份没有解释就出现的证明是一个黑箱，只是恰好带有一个经过验证的输出。这个领域可以引用它，却无法讲授它——即便该定理为真，这也是一种实实在在的损失。
这一周得出的实用建议，适用于任何购买 AI 能力（而不只是数学）的人：要求看到证据、权限，以及从一次成功的演示通向可重复工作的路径。基准测试结果与可运行的系统是两种不同的东西，而二者之间的落差，正是意外藏身之处。