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

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

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

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

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

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

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

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

传统期刊并非为这种节奏而建

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

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

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

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

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

Lean formalizations can verify logical correctness, but they can't judge whether a result is mathematically relevant or original. OpenAI is betting that its results push the boundary of human knowledge. Whether the mathematical community agrees remains an open question. So far, reactions range from excitement to frustration.

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

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

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

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