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 押注其成果推动了人类知识的边界。至于数学界是否认同，仍是一个悬而未决的问题。到目前为止，反应从兴奋到沮丧不一而足。
在最近一封公开信中，题为"AI 在数学中的严重错位"，25 位菲尔兹奖得主警告称，AI 行业的目标与数学界的目标之间存在深刻脱节。他们写道，解决问题只是实现概念理解和洞察这一真正目标的工具和替代指标。他们认为，大规模生成真命题可能会摧毁肥沃的土壤，而非催生新思想。其影响将波及到其他领域。
Gowers警告称，在一到二十年内，数学文献可能会急剧膨胀，而不再有真正理解它的人类群体存在。菲尔兹奖得主 Terence Tao 补充说，培养年轻数学家需要强调人的一面，并严格限制 AI 工具的使用，以使真正的学习和理解得以存续。