OpenAI 在 GitHub 发布 372 个 AI 生成数学证明，引发学界对形式验证与科研速度的激烈辩论

一句话结论

OpenAI 在 GitHub 开源 372 个 AI 生成的数学结果，主张形式验证可缓解传统同行评审瓶颈，但学界担忧其挤压概念创新与学术理解力。

关键要点

• OpenAI 发布 372 个由内部前沿模型生成的数学结果，目标为解决或推进公开问题，涵盖计算机算法改进与黎曼猜想进展。
• 绝大多数结果由单个 AI 代理在单次提示下生成，平均消耗约 3 小时 ChatGPT Pro Thinking 算力。
• 证明附有 Lean 语言形式化代码，支持机器可校验的逻辑正确性验证。
• 结果托管于带修订日志与引用的 GitHub 仓库，而非传统学术期刊。
• OpenAI 遵循高等研究院数学与 AI 咨询组的建议，但未公开提示词及单题算力成本。

背景与事实

2025 年，OpenAI 在 GitHub 仓库中发布了 372 个由其内部前沿模型生成的数学结果。每个结果旨在解决一个公开问题或对其做出实质性推进，内容涉及重大计算机算法优化及与黎曼猜想相关的进展。根据 OpenAI 披露，其中多数结果由单个 AI 代理在单次提示下完成，平均消耗约 3 小时 ChatGPT Pro Thinking 算力；这与此前需要一万智能体集群和数百万美元算力解决的纳维-斯托克斯问题形成鲜明对比。该纳维-斯托克斯解目前正处于为期数周的形式化审查中。OpenAI 明确将结果托管在 GitHub 而非传统学术期刊，理由是海量 AI 生成结果将超出数学界人工审查能力，因此采用 Lean 等支持机器校验的形式化语言来使形式验证成为切实可行的审查手段。OpenAI 还发布了方法论详情，包括推理过程摘要、模型尝试问题的统计及算力成本估算，并咨询了由菲尔兹奖得主 Timothy Gowers 等数学家组成的高等研究院数学与 AI 咨询组，但预设了边界：数学家仅就结果传达方式提供建议，不干涉结果是否产出或产出速度。

影响分析

对中文开发者与从业者而言，该事件揭示了形式化验证与 AI 代理在学术知识生产中的新范式。一方面，使用 Lean 等语言进行机器可校验证明的开发者可参考该仓库的方法论与算力成本模型（约 3 小时 ChatGPT Pro 算力/结果），为本地化 AI 辅助数学研究或算法验证项目提供工程参考。另一方面，OpenAI 跳过传统期刊直接开源的做法将迫使学术机构重新评估审查流程与产能瓶颈，中文高校及科研院所若希望纳入此类 AI 生成结果，需提前建立形式验证工具链与算力评估体系，而非依赖传统人工同行评审。这是基于事件事实的分析判断：OpenAI 试图以速度换取知识边界扩张，但学界对“量产真命题”的抵触可能延缓其在中文学术界的实际采纳。

适用边界

上述关于形式验证可缓解审查瓶颈的结论，在结果不具备数学相关性或原创性时不成立；Lean 形式化仅能校验逻辑正确性，无法判断结果是否推进了概念理解或具有学术价值。因此，该范式不适用于纯概念性、非形式化或强调原创洞察的数学研究领域，也不适用于缺乏形式验证工具链与算力评估能力的学术机构。

孤本观察

基于事实判断，OpenAI 在 GitHub 发布结果并预设咨询组权限边界的策略，实际上将数学界的角色从知识生产者降级为结果传达顾问，这一编辑观察凸显了 AI 行业与学术共同体在知识生产目标上的根本分歧。

来源：The Decoder