OpenAI 与 Anthropic 模型各自独立发现同一算法难题证明，Lean 验证
lxrjl · x · 2026-10-28
作者对所谓 Opus 5.5「证伪」的说法做事实核查：核心事实成立——OpenAI 称其模型于 10 月 16 日发现了对一个开放问题的否定性结果，次日用 Lean 形式化验证；Impagliazzo、Paturi、Williams 正在组织公开评审，但强调他们的参与不构成认证，如此重大的结果仍需独立审慎审查。
- 不止一家：Anthropic 次日发文称其内部 Claude 研究模型在无人类输入、1400 万输出 token 的条件下于同日独立发现核心算法，并用 Lean 形式化
- 审读过 Claude 证明的 Jelani Nelson 表示两份证明都达到约 exp(O(n/√log n)) 的运行时间
- 两大实验室独立撞车是更大的新闻，也提高了结果成立的概率
- Williams 指出「仍然很慢」的表述低估了该结果的框架意义
所属事件:OpenAI 模型宣称反驳指数时间假设，将通过独立审查(3 条相关)→
「模型」频道最新
- 同一开发者补刀:GPT-5.6 terra 若降价 80% 而非 20% 可能成爆款 — JoshPurtell · 2026-10-28
- 开发者质问 OpenAI:GPT-5.6 mini/nano 先涨价又只给 luna 降价,terra 为何不降 — JoshPurtell · 2026-10-28
- X 推出整合订阅：30 美元打包 Grok、Cursor 与 X Premium — nima_owji · 2026-10-28
- Liquid AI LFM3 用 24 层混合架构实现 256K 上下文，推理快 25% — cneuralnetwork · 2026-10-28
- 开发者列出最期待的两款模型：GLM 5.5 Flash 与 Qwen 4 27B — victormustar · 2026-10-28
- Maxime Labonne 演示 d1 模型：一次前向同时问答并框出指定物体 — maximelabonne · 2026-10-28