导语：过去几年，AI 在数学领域的角色正从“解题助手”转向“研究协作者”。它不仅能处理竞赛题、搜索证明路径，还开始接触埃尔德什问题、整数数列猜想等尚未解决的研究问题。不过，“AI 宣称找到证明”与“数学界确认问题已解决”并不是一回事。真正值得关注的进展，是 AI 生成结果开始与形式化证明、独立复现和同行评议结合，逐步形成可核验的证据链。🧠
一、最新突破：从竞赛能力走向开放问题
AI 数学能力的重要转折点之一，是系统开始输出可由证明助手检查的形式化证明。Google DeepMind 的 AlphaProof 与 AlphaGeometry 2 在 2024 年国际数学奥林匹克竞赛题目上取得相当于银牌水平的成绩，相关研究随后发表于《Nature》。这说明 AI 已能在高难度但定义明确的问题中完成较长的推理链，而不只是预测最终答案。需要强调的是，奥赛题虽然难度很高，却已有出题者设计的答案，因此不能直接等同于攻克真正的未解难题。📐 [1]
更接近数学研究前沿的是 2026 年公布的一项大规模形式化证明搜索实验。研究团队把开放问题转写为 Lean 可处理的形式化命题，再由 AI 代理反复生成、修改和编译证明。论文报告称，其性能最强的系统在测试中解决了 353 个开放埃尔德什问题中的 9 个，并证明了 492 个 OEIS 相关猜想中的 44 个。由于该成果首先以预印本形式发布，这些数字应理解为作者报告的实验结果，而不是已经完成全部同行评议的数学共识。🔍 [2]
二、为什么“形式化证明”如此关键
普通大语言模型生成的数学文字可能逻辑流畅，却在某一步偷换条件、遗漏边界情况，甚至引用不存在的定理。Lean、Coq、Isabelle 等证明助手要求把定义、前提和推理步骤写成严格的形式语言。以 Lean 为例，自动化策略最终必须产生能够被小型内核检查的证明项，因此策略程序即使存在缺陷，也不能轻易让错误证明通过内核。✅ Lean 语言参考
但“成功编译”并不代表所有验证工作都已结束。Lean 官方指南明确区分两个问题：一是形式化命题是否存在有效证明，二是该形式化命题是否准确表达了人们原本想研究的数学问题。如果形式化时遗漏假设、缩小范围，或者误解自然语言中的概念，AI 可能严谨地证明了一个“正确但答非所问”的命题。因此，机器检查解决的是推理链一致性，不能完全替代数学语义审查。⚠️ Lean 证明验证指南
三、第三方验证应包含哪些环节
- 公开完整材料：研究者应提供自然语言问题、形式化命题、证明源代码、依赖库版本、编译命令和运行环境。只发布模型回答的截图，无法支持独立检验。
- 独立环境复现：第三方需要从公开代码重新构建项目，确认不存在未完成证明、跳过内核检查的指令、不透明二进制文件或未经说明的额外公理。
- 命题一致性审查：熟悉相关领域的数学家应逐项比较原问题与形式化版本，包括量词、定义域、退化情形和隐含前提。这一步决定 AI 证明的是不是“同一个问题”。
- 新颖性检索：即使证明正确，也可能只是重新发现已有结果。验证者需要检索论文、专著、数据库和相关预印本，确认结论及证明方法是否真正具有原创性。
- 传统同行评议：形式化验证关注逻辑正确性，期刊或学术共同体还要评价结果的重要程度、解释价值、可读性以及对现有理论的影响。🧪
四、公众该如何判断“AI 攻克难题”的消息
看到类似新闻时，可以先检查三个关键词：问题是否此前公开、证明是否完整公开、是否有独立专家署名验证。如果报道只说“模型自信度很高”或“内部测试通过”，证据等级仍然较低；如果同时提供可编译的 Lean 文件、固定的软件版本和第三方复现记录，可信度就明显更高。
还要区分“开放问题”“著名猜想”和“基础性难题”。开放问题可能只是尚未在文献中解决的小范围命题，其学术价值并不低，但与黎曼猜想、P 与 NP 问题等重大难题不是同一量级。媒体若把若干专业领域中的开放子问题包装成“AI 攻克世纪难题”，容易造成误解。📢
五、AI 数学研究仍面临的限制
- 形式化成本高：大量现代数学知识尚未进入可直接调用的形式化库，研究者常需先补充定义与基础引理。
- 证明可读性不足：机器找到的路线可能非常冗长，虽然能够通过检查，却难以帮助人类理解背后的结构。
- 评价容易失真：只统计“解决数量”会忽略问题难度、既有线索、形式化提示以及人工参与程度。
- 工具链并非绝对无误：内核、依赖库与编译环境仍需版本固定、来源审计及交叉验证，不能把“软件通过”简化成无条件的真理认证。
总结：突破的核心是可验证，而非会宣布
AI 对未解数学问题的探索已经进入更务实的阶段：模型负责提出候选思路和搜索证明，形式化系统检查逻辑，领域专家核对命题含义，独立团队完成复现与新颖性审查。🚀 现阶段最有价值的变化，并不是 AI 已经可以取代数学家，而是数学研究正在建立一种“人类洞察、机器搜索、内核验证、第三方审查”的协作机制。未来真正具有说服力的突破，应当同时经得起代码编译、语义核对、文献检索和同行评议，而不是仅凭模型或开发机构的一次宣布。
