发布日期：2026-10-09 浏览：13
OpenAI发布了一批由内部前沿模型产出的大规模数学研究成果，让数学家可以访问数百项机器生成的结果。该合集出现在一个公开的GitHub仓库中，包含722篇手稿，组织为372个研究族。工作横跨纯数学、理论计算机科学和数学物理。多项结果涉及需要长链条数学推理的问题。OpenAI还在Lean中发布了许多证明的形式化版本，使计算机能够检查底层论证。
数百项成果
该仓库覆盖数论、复杂性理论、几何和数学物理等问题。一些结果还延伸到微小进展也需要大量技术工作的领域。一个例子涉及π的无理性指数。该量衡量有理数能多接近地逼近π。模型产生了一项处理该逼近数学行为的结果。另一个研究族考察NP困难性。这些问题属于计算复杂性理论，涉及被认为难以高效解决的任务。模型的工作为这一更广泛的研究体系增添了数学结果。其他手稿涉及马勒猜想、等差数列和自由群因子等问题。合集还包括量子海森堡铁磁体和相对论性Vlasov-Maxwell方程方面的工作。OpenAI将相关手稿分组为研究族，以展示各项结果之间的关联。仓库还标出了10个附有模型推理简要总结的研究族。
Lean提供检查
Lean为此次发布提供了重要的验证层。这种编程语言让研究人员能够将数学陈述和证明翻译为形式化代码。计算机随后可以检查每个逻辑步骤是否从所述假设中推出。这并不能自动确立合集中每一项研究主张都正确。许多手稿仍缺少正式的Lean版本。OpenAI表示，随着研究人员完成验证工作，将添加更多形式化内容。仓库还跟踪论文修订并提供引用指南。这让研究人员在作者更正或扩展早期手稿时有更清晰的记录。OpenAI与普林斯顿高等研究院独立的数学与人工智能咨询小组协商制定了发布流程。
模型测试了数千个问题
OpenAI还披露了其数学评估规模的细节。模型在研究过程中尝试了约4000个问题。一项被接受的结果平均消耗约三小时的等效ChatGPT Pro思考算力。公司还发布了涵盖所尝试问题和研究产出的额外统计数据。OpenAI称，推理总结让研究人员能更近距离了解模型如何处理选定的数学问题。这些总结与Lean中的形式化证明保持分离。OpenAI计划支持聚焦理解AI生成重大数学成果的研讨会、会议和特别项目。它还预计数学家的反馈将影响未来的信息披露。因此，此次发布不只是论文合集。它提供了一次测试：机器生成的数学如何以可复现的记录、计算机可检查的证明，以及对结果产生方式更高的可见度，进入研究过程。
从学术验证角度看，Lean形式化能确认证明步骤的逻辑有效性，但前提是形式化本身准确反映了原始数学陈述。大量手稿尚未形式化，意味着可检查的部分只是少数，仓库的整体可信度仍依赖人工审阅。将结果按研究族组织并附推理摘要，是在机器生成内容与人类理解之间建立中间层，但摘要不能替代同行评审。约4000个问题、平均三小时算力的披露，也说明这些成果的产出成本并不低。真正的问题在于，数学家是否愿意投入时间验证并在此基础上继续工作——如果验证成本高于独立推导，这些结果的学术价值就会受限。有观点认为，AI数学的下一步不是产出更多结果，而是建立让数学家能够验证、理解和协作的流程，否则成果数量可能超出学科消化能力。据悉，OpenAI未披露哪些结果已通过Lean完整验证，也未公布外部数学家独立复核的进展。
粤公网安备44190002007368号
