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”前沿报告、完整档案访问权限以及评论区访问权限。