AI 数学仓库更新：约 42% 顶线结果完成 Lean 形式化，撤稿 3 篇
iskander · x · 2026-10-08
danintheory 团队更新其 GitHub 数学仓库，新增 6 个 Lean 形式化、19 处修改，并撤回 3 篇，目前仓库约 42% 的顶线结果（top-line results）已完成形式化，团队将持续更新形式化与勘误。
顶级数学家 Terence Tao（转发者 littmath 即为其账号）评论称，其中一篇被撤回的手稿是他此前试图理解的《K3 曲面的 Kuga–Satake 对应的代数性》，问题本身他很喜欢，原思路看起来令人兴奋但现在已不明确。他指出：对人类作者的手稿，即使论证有错也常能从中提取有价值的直觉，而这批 AI 生成的形式化是否还能这样利用并不清楚；他的经验是 AI 在这类「模糊任务」上帮助不如预期。
所属事件:OpenAI 数学仓库因符号错误撤回 3 篇霍奇猜想论文(5 条相关)→
「模型」频道最新
- 马斯克转发力挺:Grok 机器人账号表现「确实这么强」 — elonmusk · 2026-10-09
- 曝 Claude 模型将首次登陆 Gemini 平台,与 Gemini 系列并列服务企业客户 — testingcatalog · 2026-10-09
- 同一 Xbox 手柄 prompt 测 371 个模型，作者建成模型博物馆 — sirjoaco · 2026-10-09
- 博主预测 Fable 与 Astra 至少两周后发布，Gemini 4 Argon 或短暂登顶 — bindureddy · 2026-10-09
- 网友实测 LightOnOCR-3:建议拿最难的文档样例挑战它 — IgorCarron · 2026-10-09
- OpenAI 与 Claude 拒帮忙逆向工程，用户改用 Kimi 绕过限制 — doodlestein · 2026-10-09