OpenAI 开源内部模型产出的 722 篇数学成果手稿与形式化证明

OpenAI 在 GitHub 开源了由内部前沿模型生成的 722 篇数学手稿，归入 372 个成果族并涵盖准黎曼猜想、四维挂谷猜想等长期悬而未决的难题。绝大多数结果平均单项消耗约 3 小时 ChatGPT Pro 思考算力，其中 235 族附带了 Lean 形式化证明。该批成果在展示批量定理证明能力的同时，也引发了数学界关于论文规范、引用伦理以及专家审读验证成本错配的广泛讨论。