OpenAI 公开模型生成的数学成果、Lean 形式化与过程材料。
OpenAI 发布模型生成的数学成果与 Lean 验证
2026-10-06前沿观察WATCH
OpenAI 又公开三项模型生成的研究主张，覆盖调和分析、复杂性理论和量子场论，并尝试由外部学者组织复核。团队公开了“所有维度 local smoothing”结果的自然语言证明与 Lean 形式化，也公开了反驳 Exponential Time Hypothesis 的自然语言和 Lean 证明。OpenAI 明确把这些稿件视为原始研究数据；独立团队尚未形成广泛认可。
可用状态：成果公开；生成模型未开放
对你意味着什么
对 AI 科研团队来说，重点正从“模型声称发现了什么”转向公开产物、依赖追踪和独立解释。Lean 能检查形式化命题是否由给定公理推出，但不能自动证明形式化命题完整对应研究者想表达的科学结论。
前沿观察
公开材料与效果验证，分开看。
已记录的事实是工作及其材料已公开。论文或作者报告的效果不自动等于独立复现。下一步关注可复用代码、任务设置和第三方验证。
证据与关联材料
OpenAI 因符号错误撤回三篇稿件、修订 14 篇，并报告 Lean 覆盖达到 300/719。
OpenAI 公开 local smoothing / Kakeya 与 ETH 主张的自然语言和 Lean 产物，并把结果称为等待学界解释的原始研究数据。
后续变化
OpenAI 撤回三篇模型生成的数学稿件并修订 14 篇
OpenAI 公开三项新的模型生成研究主张并引入外部 shepherd
技术细节与六维评分
| 公开材料 | 论文、Lean 形式化、修订与引用规范、10 份推理摘要 |
|---|---|
| 报告算力 | 每项成果平均约等于 ChatGPT Pro 三小时思考量 |
| 可用性 | 成果公开；生成模型未开放 |
| 验证边界 | Lean 覆盖许多但未必全部证明；专家复核仍在继续 |
| 2026-10-08 更新 | 一个符号错误使核心构造与两篇依赖论文失效，三篇稿件被撤回；另修订 14 篇、更新 13 篇依赖引用，top-line Lean 覆盖为 300/719（约 42%）。 |
| 2026-10-26 更新 | 新增 local smoothing / Kakeya、Exponential Time Hypothesis 与量子场论三项主张 |
| 发布方式 | 数学产物公开；计算机科学产物公开并由外部协作组解释；物理产物暂缓公开，等待协作者自行撰写 |
| 2026-10-26 验证边界 | OpenAI 将稿件称为原始研究数据；广泛独立认可尚未形成 |
| 2026-10-26 时间依据 | OpenAI RSS 发布于 2026-10-26T14:30:00Z；上一轮快照未出现，按 overlap 补录 |
技术影响 4
工程价值 3
采用信号 2
成熟度 2
验证成本 4
风险 3