检测到您的浏览器版本过低，可能导致某些功能无法正常使用，建议升级您的浏览器，或使用推荐浏览器 Google Chrome 、Edge、Firefox 。 X
继纳维－斯托克斯方程成果公布不久之后，OpenAI披露其在第二项千禧年难题——霍奇猜想上取得实质性进展。霍奇猜想是七大千禧年难题中隶属于代数几何领域的核心难题，由英国数学家威廉·霍奇于上世纪五十年代提出，主要研究复代数簇上代数闭链与上同调类之间的对应关系。该猜想有效串联起拓扑、几何与代数三大数学分支，理论体系高度抽象，是现代代数几何的重要基础问题。数十年来，学界始终未能形成完整确定的证明，其理论理解与研究门槛显著高于纳维－斯托克斯方程。
与NS方程成果的快速公开不同，OpenAI并未第一时间完整公布霍奇猜想的证明文本，而是采取更为审慎的发布策略：先交由独立数学家顾问小组预审核验，再逐步对外公开研究材料，规避过度舆论炒作带来的学术争议。本文将从当前AI数学研究的主流路线、业内评价与反馈、未来发展趋势几部分进行说明。
1. 当前 AI 数学研究的三条主流技术路线
当前前沿AI数学研究领域尚未形成标准化、统一化的技术范式。Google DeepMind、Anthropic、OpenAI三大头部科技机构基于自身技术积淀与研究目标，形成了截然不同的技术路线。
Google DeepMind是业内最早系统性布局AI数学自动证明研究的团队。2024年，该团队发布AlphaProof与AlphaGeometry 2两大系统，模型能力达到国际数学奥林匹克竞赛（IMO）银牌水准，成功解答当年赛事6道真题中的4道。其核心技术为经典的神经符号双系统架构，分工明确、逻辑清晰。有如下特点：
（1）语言模型基于Gemini架构搭建，依托海量数学文献、定理案例完成预训练，能够自主挖掘数学逻辑规律，生成候选证明思路与构造方案；
（2）符号推理引擎依托Lean证明器与AlphaZero式强化学习搭建，在标准化形式化语言框架内，逐步拆解、推导证明步骤，逐行验证逻辑严谨性。AlphaGeometry创新性生成1亿条合成几何定理与证明样本用于模型训练，摆脱了对人类现有证明数据的依赖。
2026 年 9 月，Anthropic 宣布 Claude 用11 天时间完成了费马大定理的端到端 Lean 形式化证明。这是历史上第一个完全由计算机内核类型检查通过的费马大定理形式化版本。其技术路线与 OpenAI 形成鲜明对比，有如下几方面特点：
（1）单模型长时间运行：一个 Claude 智能体群体在 Prove2Me 平台上持续工作 11 天，消耗约 60 亿输出 token，生成约 1300 万行 Lean 代码，证明约 30300 个定理；
（2）端到端自主：从命题陈述出发，仅使用 Lean 三条标准公理，自主生成从公理到结论的完整 Lean 代码，不依赖人工分步引导；
（3）成本更低：Anthropic 路线用OpenAI约几十分之一的资源完成了一项已有人类证明的形式化工作，验证了现有人类数学成果可以被 AI 大规模形式化。
OpenAI 在 NS 项目上的路线为：智能体分组协作，组内通信，有权访问互联网缓存和代码执行工具，由 Codex 做跨组洞见汇总。约 1 万个并发智能体运行88 小时、累计270 万条消息、1300 亿输出 token。这条路线的特点是：
（1）不追求单模型的深度推理能力，而是靠数量级的算力碾压覆盖尽可能多的证明搜索空间；
（2）智能体之间不是简单的分工，而是类人的数学研究协作，由不同小组尝试不同构造思路，互相启发；
（3）成本极高（数百万美元），但能在极短时间内（88 小时）探索人类团队需要数年才能遍历的构造空间。
这三条路线各有取舍， 分别适用于不同类型的数学问题。
2. 业内评价与反馈：两极分化的学界观点
正面评价：AI成为全新数学科研工具
以部分青年数学家为代表的支持者认为，AI极大拓展了数学研究的探索边界。传统人类数学家受限于大脑算力，很难同时遍历成千上万种构造方案；AI可以快速搜索人类难以想到的结构。陶哲轩提出，数学研究正在从证明稀缺时代走向证明过剩时代，AI能够快速产出大量可验证的候选证明，数学家的角色从“完成全部推导”转变为解读证明、提炼内在思想。同时形式化证明工具可以减少传统论文中的低级逻辑错误，提升数学成果可靠性。
研究者指出，AI擅长完成冗长、重复、繁杂的代数推导与构造搜索，将数学家从繁琐机械推导中释放，把精力投入提出猜想、洞察数学结构等高创造性工作。从历史上看，计算机辅助证明早有先例（如四色定理），而当前大模型+形式化证明体系，是计算机辅助数学的跨越式升级。
质疑与担忧：证明可读性、学术归属与科研生态风险
持审慎批评态度的数学家提出多重质疑。第一，证明可读性问题：AI 产出证明往往篇幅庞大，步骤繁琐，逻辑迂回，缺少人类数学里的核心洞察。即便计算机验证逻辑正确，人类也很难读懂，无法从中提炼出新数学思想，被学者称为“无味证明”。
第二，学术贡献归属争议，NS的爆破构造思路源自前人已发表研究，AI是在已有框架下完成海量搜索，那么核心功劳属于AI，还是提出研究路线的人类数学家？
第三，科研生态风险：AI企业把千禧难题、顶级猜想作为大模型宣传素材，容易出现媒体过度简化、夸大成果，混淆“形式逻辑成立”和“通过学界同行评议”两个概念。同时，部分菲尔兹奖得主联名发文，指出数学的目标不仅是得到一个可验证结论，单纯以破解难题作为性能基准，会损害数学基础研究本身。
3. 核心辨析：AI暴力推演 vs 人类的直觉与优雅证明
人类数学家的优雅证明，核心是直觉洞察：数学家在长期积累下感知对象内在结构，找到巧妙引理，用简短思路直击问题本质，剥离冗余细节，把复杂问题转化为简单命题。证明不只是篇幅短，更重要是揭示了不同数学分支之间隐藏联系，带来新的数学思想，启发后续大量研究。而AI只要找到一条合法逻辑链就停止优化，不在乎证明篇幅、是否便于人类理解，因此经常生成冗长、迂回的证明。AI缺少人类那种一眼洞察全局结构的数学直觉。
二者的差异可以概括为：AI擅长寻找满足约束的逻辑路径，但缺少对数学美感、结构意义的理解；人类追求理解与洞见，追求简洁优美的证明，而优美证明往往可以催生新理论。但同时要注意，许多人类早期证明同样冗长晦涩，简洁优雅版本是多年反复提炼、简化后的产物。AI产出的复杂证明，未来也有可能在人类数学家的解读、重构之下，被提炼出简洁优雅版本。
因此二者不是非此即彼的对立关系。AI可以作为搜索、验证工具；人类负责洞察、提炼、简化，发掘证明背后的数学思想。
4. AI辅助数学研究的未来发展趋势
第一，人机协同将成为前沿数学研究常态。AI负责大规模搜索、海量符号演算、形式化校验；人类数学家提出猜想、选择研究方向，解读AI输出结果，提炼数学思想。AI不会直接替代顶尖数学家，而是改变数学家的工作模式。
第二，形式化数学会逐步普及。Lean等定理证明将会变成数学论文标准校验手段，未来顶尖期刊更可能接受附带形式化验证代码的论文，降低证明漏洞风险。
第三，评价体系需要调整。AI产出成果出现之后，学界需要建立新的评价框架，区分“证明逻辑正确性”和“数学洞见价值”，避免单纯以是否破解难题评判成果价值。
第四，研究伦理与传播规范。AI数学成果发布时，应当严格区分阶段性进展和最终定论，配合独立数学家评审，防范商业宣传过度夸大，保护纯粹数学的学术生态。
参考资料：
[1] DeepMind. AI achieves silver-medal standard solving International Mathematical Olympiad problems[EB/OL].(2024-07-25)[2026-09-22].https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/.
[2] Anthropic. Learning more about Claude's mathematical capabilities[EB/OL].(2026-08-10)[2026-09-22].https://www.anthropic.com/research/riemann-zeta.
[3] Anthropic. Formalizing Fermat's Last Theorem in Lean[EB/OL].(2026-09-04)[2026-09-22].https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf.
[4] 新智元. AI 又拿下一个千禧年难题？OpenAI 总裁亲口证实「进展重大」[EB/OL].(2026-09-18)[2026-09-22].https://hub.baai.ac.cn/view/58065.
[5] Lamzouri Y. A New Proof that More Than 2/3 of the Zeros of the Riemann Zeta Function are Simple and on the Critical Line[EB/OL].(2026-09-07)[2026-09-22].https://arxiv.org/pdf/2609.02882.
[6] Becker P, Greger M, Peters D. Existence of the Core in Approval-Based Committee Elections[EB/OL].(2026-09-12)[2026-09-22].https://arxiv.org/pdf/2609.11912
