OpenAI丢722篇数学手稿 内置前沿模型独立产出

## OpenAI 丢 722 篇数学手稿 内置前沿模型独立产出 OpenAI 10 月 6 日在官方研究博客发文，公布内部前沿模型（代号未披露）独立产出的数学研究合集，包含 722 篇手稿、372 个结果族，覆盖约 4000 道数学问题，其中相当一部分附带 Lean 4 形式化证明可供计算机自动校验。这是继 9 月「用一个月训练解决 100 道数学难题」之后，OpenAI 规模最大的一次数学研究成果公开。 本次发布的核心亮点在「可验证」：OpenAI 同时上线 GitHub 仓库 openai/ten-proofs 与 openai/math，前者收录 10 篇代表性论文对应的 Lean 4 证书，后者包含全部 722 篇手稿与支撑证明；外部数学家可直接通过 Lean proof assistant 复核每一步论证，无需依赖模型本身的可信度。OpenAI 还附上模型推理过程的 10 篇摘要文档，公开平均单题消耗约 3 小时推理算力。 研究风格上，OpenAI 将这次发布明确定位为「research drop, not a launch」：不公布模型名称、不开放 API、不承诺后续迭代节奏，仅作为学术成果公开。这种「先发论文再发产品」的做法与 Google DeepMind、Anthropic 近半年的策略形成对比，也被业内视为 OpenAI 在 AGI 叙事受挫后转向「先建可信度、再扩商业化」的阶段性选择。 值得注意的是，Anthropic 10 月 6 日同日宣布 Claude 解决了 Terence Tao 等菲尔兹奖得主长期关注的「随机矩阵猜想」，与 OpenAI 此次大规模数学合集形成隔空对照。两大前沿实验室不约而同地押注「AI for Math」，意味着 2026 年下半年数学很可能成为继代码之后，又一被 AI 实质突破的科研领域。 --- **参考来源：** 1. OpenAI 官方研究博客 — Sharing AI progress in mathematics：https://openai.com/index/sharing-ai-progress-in-mathematics/ 2. GitHub 仓库 — openai/ten-proofs：https://github.com/openai/ten-proofs 3. Interesting Engineering — OpenAI's largest math release tackles 4,000 problems with Lean proofs：https://interestingengineering.com/ai-robotics/openai-largest-math-release-lean-proofs 4. Digital Applied — OpenAI Astra: Ten Solved Math Problems, Zero Product：https://www.digitalapplied.com/blog/openai-astra-ten-math-proofs-lean-announcement 5. Shattered.io — OpenAI Drops 722 Math Papers From a Hidden Model：https://shattered.io/openai-722-math-manuscripts-hidden-model-2026/ 6. OpenAI Research Index：https://openai.com/research/index/ 7. Reddit r/mathematics — Is formalizing mathematics in Lean the biggest bottleneck for AI：https://www.reddit.com/r/mathematics/comments/1vdpj5o/is_formalizing_mathematics_in_lean_the_biggest/ 8. The Decoder — OpenAI says its internal model solved over 100 long-standing math problems：https://the-decoder.com/openai-says-its-internal-model-solved-over-100-long-standing-math-problems-after-just-a-month-of-training/