OpenAI 在 GitHub 发布 372 个 AI 生成数学证明

OpenAI 发布了一大批由内部 AI 模型生成的数学成果。这些证明发布在 GitHub 上，而不是学术期刊中，旨在通过形式化验证让审查更具可行性。

OpenAI 发布了由内部前沿模型生成的 372 项新的数学成果。每项成果都被认为旨在解决一个开放问题，或朝着解决该问题取得实质性进展。该合集包括对重要计算机算法的改进，以及与黎曼猜想相关的进展。

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

OpenAI 表示，几乎每项成果都来自对单个 AI 智能体的一次提示，尽管有些需要多次尝试。这与Navier-Stokes 解形成鲜明对比，后者需要由 10,000 个智能体组成的群体，并耗费数百万美元的算力。平均而言，每项成果大约消耗了相当于三小时的 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”前沿报告、完整档案访问权限，以及进入我们评论区的权限。