ARTICLE · 1139372

AI研究热点|OpenAI公开722份数学稿件,部分证明附Lean形式化材料

发布时间：2026-10-08 12:27:26 最近访问：2026-10-08 12:27:27

◆OpenAI公开数学稿件，验证状态随仓库一起披露

OpenAI在10月6日发布数学研究进展，将内部前沿模型产生的数学稿件与证明材料放入GitHub仓库。截至核对时，目录包含722份稿件，归入372个结果族；同一族可以包含主要结果、配套论证、推论或不同证明，所以稿件数量不等于独立解决问题的数量。

材料的验证程度并不统一。部分证明附有Lean形式化内容，另一些尚未完成形式化；仓库明确提示，未形式化结果可能存在问题，并会继续修订。Lean提供机器可检查的证明表达，但是否覆盖某一稿件、使用哪些假设和验证配置，仍要看对应目录，不能仅凭仓库存在Lean代码就替全部论文背书。

OpenAI还公开了10份模型推理摘要、尝试问题数量及算力估算。其说明称，模型在评估中尝试约4000个问题，绝大部分结果使用相同流程产生，每项结果平均消耗约相当于ChatGPT Pro思考三小时的算力；这是计算资源等值估算，不能直接换算为普通用户实际等待三小时即可复现。

对重大猜想相关结果，也要保留题目里的条件。仓库举出的例子包括黎曼ζ函数的特定无零区域，以及CM阿贝尔簇上的霍奇猜想结果，并没有据此宣布完整黎曼猜想或所有情形的霍奇猜想已被解决。公开稿件、形式化证明和学界复核是不同环节，后续价值取决于具体论证能否经受检查与修订。