OpenAI 在 GitHub 发布 372 项 AI 生成数学结果，称学术评审跟不上节奏

OpenAI 发布了一个由内部 AI 模型生成的大量数学成果集合。这些证明发布在 GitHub 上而非学术期刊上，并采用了形式化验证以使审阅更加可行。

OpenAI 发布了由内部前沿模型生成的 372 项新数学成果。每一项成果都声称解决了一个未解问题或取得了实质性进展。该集合包括对主要计算机算法的改进以及与 黎曼猜想相关的进展。

该公司将这些成果托管在 GitHub 仓库中，并附有修订日志和引用。据 OpenAI 称，同一个模型此前已经产出了一个 Navier-Stokes 问题的解决方案，该方案已经经过了数周的正式审查。

OpenAI 表示，几乎每一项成果都来自对单个 AI 智能体的单次提示，不过有些需要多次尝试。这与 Navier-Stokes 解决方案形成了鲜明对比，后者需要 10,000 个智能体组成的集群以及数百万美元的计算资源。平均而言，每项成果消耗了大约三个小时的 ChatGPT Pro Thinking 计算资源。

形式化验证可能缓解审阅瓶颈

许多证明都附带了 Lean 形式化，这是一种为机器可检验的数学证明而构建的编程语言。更多形式化工作正在计划中。原因很实际：AI 生成成果的庞大数量很容易超出数学界人工审阅的能力。

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

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

OpenAI 将其成果发布在 GitHub 而不是同行评审期刊上。这是一个表态性的举动，因为它暗示传统的科学研究流程对于如此体量的潜在新知识来说太慢了。

OpenAI 咨询了高等研究院数学与人工智能咨询小组，并大致遵循了他们的公开建议，不过该公司没有发布任何提示，也只分享了平均计算成本而非每个问题的具体数字。该咨询小组包括菲尔兹奖得主 Timothy Gowers 以及其他知名数学家。

该公司还宣布计划资助专注于理解 AI 生成成果的研讨会和会议。OpenAI 承认希望改进其引用和呈现的质量，并表示正在努力以负责任的方式发布该模型，以"直接赋予科学家最先进的能力"。

不过，OpenAI 事先为咨询小组设定了一个重要界限：数学家可以就成果如何传播提供建议，但不能就成果是否产出或产出速度提供建议。

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

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

在最近一封题为《人工智能在数学中的严重错位》的公开信中，25位菲尔兹奖得主警告称，人工智能行业的目标与数学界的目标之间存在深刻脱节。他们写道，解题仅仅是工具，是通往概念性理解与洞见这一真正目标的替代指标。他们认为，大规模产出真命题可能会摧毁沃土，而不是催生新的思想。其影响将波及到其他领域。

高尔斯警告说，在一到二十年内，数学文献可能会急剧增长，而与此同时，将不再有任何人类群体真正理解它。菲尔兹奖得主陶哲轩补充说，培养年轻数学家需要强调人的一面，并严格限制人工智能工具的使用，以便真正的学习和理解得以存续。

没有炒作的人工智能新闻——由人类策划

订阅 THE DECODER，享受无广告阅读、每周人工智能通讯、我们每年六期的独家“AI Radar”前沿报告、完整档案访问权限以及评论区访问权限。