OpenAI 证明手稿六大命题已 Lean 形式化，可用 Comparator 工具验证
maier_ak · x · 2026-10-29
这份 OpenAI 模型手稿的独特之处：六个主要命题已在 Lean 中形式化，可用开源 Comparator 工具在仅三条标准公理下检验；其中被信任的命题读起来与标准猜想一致。作者同时提醒：尚缺专家公开确认形式化陈述与猜想完全对应，也无人公开审读论证本身，OpenAI 自己也只称其为原始研究数据。
所属事件:传 OpenAI 模型以 Lean 证明 Kakeya 等猜想，待专家评估(5 条相关)→
「研究」频道最新
- AI 发现快过验证机构：AlphaFold 绘 2 亿蛋白结构背后的科研诚信悖论 — mikeflache · 2026-10-29
- FrontierCS 2 排名洗牌：Claude Opus 5.5 居首，DeepSeek 1017 被指退化 — teortaxesTex · 2026-10-29
- 不到 500 美元给开源模型做「宪法」人格训练:grafting 绕开 44 万美元成本 — voooooogel · 2026-10-29
- 研究者把 Transformer 层改造成完整符号 CPU — yshan2u · 2026-10-29
- 750K 参数 NanoDreamer:MacBook M5 上自训世界模型打 5 款游戏 — CatAstro_Piyush · 2026-10-29
- 为什么不能直接去掉 Transformer 的位置编码？答案是置换等变性 — cneuralnetwork · 2026-10-29