GPT-5.6 使用一个提示词填补了凸优化中 30 年的空白
一款 AI 模型（GPT‑5.6 “Sol Pro”）借助一个十页、由专家精心撰写的提示词，并在后续由 Lean 定理证明器验证，帮助证明了凸优化中一个已有 30 年历史的开放结果。评论者讨论了该系统到底贡献了多少真正的新意，还是仅仅充当了一个极其强大的自动化助手，以及这对数学家和程序员未来角色意味着什么，尤其是在“低垂果实”和“中等低垂果实”问题上。讨论进一步扩展到：大语言模型是否只是“随机鹦鹉”、它们可能多快在各个领域取代人类工作，以及如果 AI 持续进步，社会与经济需要作出哪些变化。
结果的范围以及获得方式
- 评论者指出，这个证明已通过 Lean 验证，但尚未经过同行评审，因此其状态是“有前景但仍属暂定”。
- 关键细微之处在于：GPT‑5.6 Sol Pro 使用了一个约 10 页、由领域专家撰写的提示词，而这建立在此前一年人类工作的基础上（包括更早的 LLM 辅助尝试）。
- 这被视为强有力的证据，表明当路径可以通过现有技术抵达时，LLM 能够补上缺口，但并不是那种“输入‘把它解决了’然后走开”的自主能力。
对数学和研究职业的影响
- 一些人认为，数学/理论计算机科学中低垂果实和“中等低垂果实”会越来越多地被交给 AI，人类则转向真正新颖的想法和问题选择。
- 另一些人担心，这会削弱传统训练路径，因为初级研究者正是通过这些问题来磨炼技能的。
- 还有人把这与软件行业类比：初级人员和“照方抓药者”会最先被替代；而深厚的领域理解和系统级理解仍然重要。
LLM：智能、创造力与“随机鹦鹉”之争
- 支持者认为，解决 30 年难题并对其他猜想作出贡献，反驳了“只是鹦鹉”的观点，显示出真正的推理能力。
- 怀疑者则坚持认为，LLM 是建立在人类生成模式之上的复杂预测引擎，并不真正具备创造力或理解力。
- 有人指出，如果这都不算“智能”，那这个词就失去意义；也有人回应说，统计式模式匹配加上暴力搜索就足以解释这一切。
提示词、代理系统与“框架工程”
- 多条评论强调，写好提示词和流程更接近流程/框架工程，而不是“魔法式提示”。
- 讨论中提到了多代理系统（Pro 对比 Ultra），模型在其中以循环方式进行规划、执行、测试和自我批评。
- 人们也注意到，LLM 还能帮助生成它们自己的提示词和工作流，从而随着时间推移减少手工提示设计的需求。
形式化验证与证明基础设施
- Lean 被强调为当今相当于旧系统如 Mizar 的对应物；机器检查证明被视为信任 AI 生成数学内容的关键。
- 有些人希望看到 LLM 通过完全形式化来处理非常长或难以理解的证明（例如大型分类定理）。
更广泛的社会与经济担忧
- 反应从兴奋（“智能很便宜，我们可以加速科学”）到焦虑（担心失业、分层和“技术封建主义”未来）不等。
- 还有人认为真正的问题是政治经济：收益如何分配，而不是数学本身。