OpenAI 在 GitHub 发布 372 条 AI 生成的数学结果，称学术界需跟上

OpenAI 发布了一批由内部 AI 模型产生的大量数学成果。这些证明发布在 GitHub 而非学术期刊上，旨在通过形式化验证使审阅更切实可行。

OpenAI 发布了由其内部前沿模型生成的 372 项新数学成果。每项成果理应解决一个开放问题，或在其中取得实质性进展。这批成果包括对重要计算机算法的改进，以及与黎曼猜想相关的进展。

该公司将这些成果托管在一个 GitHub 代码库中，并附有修订记录和引用信息。据 OpenAI 介绍，同一模型此前还给出了一个 Navier-Stokes 问题的解，目前该解已接受形式化审查数周。

OpenAI 表示，几乎每项成果都来自对单个 AI 智能体的单次提示，尽管有些经过了多次尝试。这与Navier-Stokes 解形成鲜明对比——后者需要一万个智能体组成的集群以及价值数百万美元的算力。平均而言，每项成果消耗的算力大约相当于三小时的 ChatGPT Pro Thinking 计算量。

形式化验证有望缓解审阅瓶颈

许多证明附带了 Lean 形式化版本，Lean 是一种专为可机器校验数学证明而设计的编程语言。更多形式化版本正在规划中。原因很实际：AI 生成成果的庞大规模很容易超出数学界人工审阅的承受能力。

OpenAI 还公布了其方法论的细节，包括推理过程的摘要、模型尝试问题数量的统计数据，以及算力成本的估算。

传统期刊无法适应这种节奏

OpenAI 将成果发布在 GitHub 上，而非同行评审期刊。这一举动本身颇具表态意味，因为它意味着传统的科学研究流程对于这一规模的潜在新知识而言过于缓慢。

OpenAI 咨询了高等研究院数学与人工智能咨询小组，并大致遵循了他们的公开建议，不过该公司并未公开任何提示词，且只分享了平均算力成本，而非逐题数据。该咨询小组成员包括菲尔兹奖得主 Timothy Gowers 等知名数学家。

该公司还宣布计划资助以理解 AI 产出成果为主题的研讨会和学术会议。OpenAI 承认希望改进其引用和呈现的质量，并表示正在负责任地发布该模型，以"直接为科学家提供最先进的能力"。

不过，OpenAI 事先为咨询小组设定了一条重要界限：数学家可以就成果的传播方式提出建议，但无权干预是否产出成果以及产出的速度。

数学界对批量生产的证明究竟意味着什么存在分歧

Lean 形式化可以验证逻辑正确性，但无法判断一项成果在数学上是否具有重要性或原创性。OpenAI 押注其成果能拓展人类知识的边界。数学界是否认同，仍是一个悬而未决的问题。到目前为止，外界的反应从兴奋到沮丧不一。

在最近一封题为《AI 与数学的严重错配》的公开信中，25 位菲尔兹奖得主警告称，AI 行业的目标与数学的目标之间存在深刻的脱节。他们写道，解题只是实现概念理解与洞见这一真正目标的工具和代理。他们指出，批量生产真命题可能会摧毁沃土，而非催生新思想。其影响还会外溢到其他领域。

Gowers 曾警告说，在一二十年内，数学文献可能会急剧膨胀，而不再有任何真正理解它的人类社群。菲尔兹奖得主 Terence Tao 补充说，培养年轻数学家需要强调人的那一面，并严格限制 AI 工具的使用，从而让真正的学习与理解得以存续。

没有炒作的 AI 新闻 – 由人工精选

订阅 THE DECODER，即可享受无广告阅读、每周 AI 时事通讯、每年六期的独家“AI Radar”前沿报告、完整档案访问权限，以及评论区的使用权限。