研究者在 Lean 中验证改进 OpenAI 数学证明结果
Eliv_nurotic · reddit · 2026-10-08
有研究者声称已在 OpenAI 近期数学成果基础上做出显著改进，并通过 Lean 形式化验证，代码公开在 GitHub（CrocSwap/integer-mult-bounds）。发帖人以此反驳「从这些 AI 生成证明里学不到东西」的质疑，认为 AI 辅助数学证明已有实质进展。
所属事件:研究者用 Lean 验证并改进 OpenAI 数学证明(2 条相关)→
「研究」频道最新
- LightOnOCR-3 训练秘辛：用 OCR 参考文本引导逻辑分块 — IgorCarron · 2026-10-09
- LightOnOCR-3 揭示：单一版面模型无法覆盖全部文档类型 — IgorCarron · 2026-10-09
- Text2Sim 用文本生成物理仿真场景，输出可编辑的真物理视频 — erwincoumans · 2026-10-09
- 单张图像重建 3D 场景:Building Rome 项目可见范围外几何也补全 — jonstephens85 · 2026-10-09
- PredActor 用单一扩散策略统一人形机器人运动生成与控制,G1 端侧跑 50Hz — carlosdponx · 2026-10-09
- 研究称持续学习无需 on-policy,正确的 off-policy 训练同样有效 — AdtRaghunathan · 2026-10-09