OpenAI公开722份数学稿件，核验工作才刚开始

AI for Science / 数学 · 9.7/10 · 建议深挖

OpenAI 公开了数学成果合集及其 GitHub 仓库。仓库目前列出 722 篇手稿，归入 372 个结果家族；同一研究问题可能有主结果、补充论证和不同证明，因此不能把“722 篇”直接读成“722 个已经解决的公开难题”。OpenAI 还给出约 4000 道尝试过的问题、十份模型推理摘要和部分 Lean 形式化证明。Lean 能按明确的公理与规则检查写进去的推导步骤，但不是给整批论文盖上同行评审印章。

这次发布改变了问题的规模。过去谈“AI 做数学”，常常围绕一两道题和演示视频；现在研究者面对的是一整座可下载、可引用、会继续修订的手稿库。模型负责大量提出候选证明，数学界则要检查结果是否真是新发现、定理条件有没有写对、证明是否完整，以及同一结果是否已经存在于文献中。公开仓库还保留版本修订路径，让后续纠错有出处。这种生产与核验速度的不对称，可能比手稿总数更值得研究。

必须把成果状态说准。仓库说明明确承认并非所有结果都配有 Lean 形式化，未形式化稿件可能有问题；公开的也不是产生它们的内部模型。OpenAI 给出的平均计算量约为每项三小时 ChatGPT Pro 等价推理，并不能据此推算每个结果的真实研究成本。今天可以确认的是材料已经开放供数学家检查，不能据此宣称其中每项重大猜想都已被学界接受。具体哪几项经得起审查，要靠逐篇后续工作回答。