模型助力解决30年优化难题
pkerger · reddit · 2026-07-17
作者称自己用一套模仿 OpenAI CDC 证明项目的提示方法，让模型在一次 148 分钟会话中给出了解决方案，并且已经用 Lean 形式化验证通过。
主要内容
- 研究对象是一个存在于凸优化/复杂度理论中的 30 年开放问题。
- 作者是伯克利 IEOR 教授，强调结果尚未同行评审。
- 他认为这套 prompt + 模型协作方式，可能对理论计算机科学和数学开放问题有更大潜力。
额外信息
- 作者给出了 Medium 文章、GitHub 仓库、Lean 代码、完整 prompts 和构建说明。
- 还提到自己之前尝试用更早版本模型未成功，而这次在新版本上“一次成”。
所属事件:GPT-5.6接连破解多年未解数学难题(4 条相关)→
「研究」频道最新
- 斯坦福数据中心化 AI 研讨会开放报名，海报截止延期 — jure · 2026-10-26
- 「氛围验证」研究：近 60% 的形式化证明证明的不是作者本意 — basedjensen · 2026-10-26
- 浏览器助手 Ito 读懂浏览意图，自动把标签页编排成 Flows — andrewkuznet · 2026-10-26
- 康奈尔研究称大脑按线性序列处理语言,挑战乔姆斯基层级语法;印度语言成反例讨论点 — anirbanbandyo · 2026-10-26
- Hi3D V1.0 开源发布：训练资产翻四倍，切片成功率 90% — kimmonismus · 2026-10-26
- Ortet 首次健康评测：34 个开源模型跑 50 项任务，综合排名不够用 — elmanmansimov · 2026-10-26