AI攻克顶级数学难题，数学家的“智能伙伴”已上线？

一个悬置五年的猜想

数学的世界里，时间以独特的方式流淌。五年，对于一个悬而未决的猜想来说，或许只是弹指一挥间。五年前，数学家陈大卫（Dawei Chen）与昆汀·詹德隆（Quentin Gendron）在代数几何的崎岖山路上艰难跋涉。他们试图厘清一个关于曲面距离测量的复杂定理，却意外地撞上了一堵坚硬的墙——一个他们无法证明也无法绕开的、来自数论领域的奇特公式。

如同登山者在冲顶前发现关键装备缺失，他们不得不止步。最终，这篇本该是定理的论文，只能以“猜想”的形式公之于众，留下一个优雅而遗憾的问号。陈大卫曾尝试用ChatGPT寻找灵感，花费数小时提示、引导，但AI的回应始终在门外徘徊。这个难题，仿佛成了一块试金石，考验着人类智慧的边界。

一场会议与一夜之间的“神谕”

转机出现在华盛顿的一场数学会议上。在一次招待酒会中，陈大卫遇到了著名数学家小野健（Ken Ono）。小野健的人生轨迹刚刚发生了一次剧变——他辞去了弗吉尼亚大学的终身教职，加入了一家名为Axiom的人工智能初创公司。这家公司的联合创始人，正是他曾经指导过的得意门生，24岁的华人天才少女洪乐潼（Carina Hong）。

陈大卫向小野健倾诉了那个困扰他五年的猜想。故事的戏剧性在第二天早晨达到了高潮。小野健带着一份完整的证明找到了陈大卫，而这份证明的作者，正是Axiom公司的数学AI——AxiomProver。

“在那之后，一切都豁然开朗。”陈大卫回忆道。AxiomProver不仅找到了解开谜题的钥匙，更揭示了一条被所有人类数学家忽略的路径。它将这个代数几何问题与一个19世纪的数论现象联系起来，构建了一套完整的证明，并自行完成了验证。小野健说：“AxiomProver发现的，是所有人都错过的东西。”

这并非孤例。在最近几周，AxiomProver接连攻克了多个长期悬而未决的数学难题，包括一个与传奇数学家拉马努金百年前的笔记相关的猜想。在那个案例中，AI甚至独立完成了从头到尾的全部证明工作。

“智能伙伴”如何思考？

AxiomProver的成功，并非简单依赖于大型语言模型的概率猜测。它的核心是一种**“混合智能”**的架构，将大型语言模型的广博知识与一个名为Lean的形式化验证语言相结合。Lean是一种专门的数学语言，它能将抽象的数学概念转化为计算机可以严格执行和验证的代码。

这种模式赋予了AI一种全新的能力：

• 超越检索的创造力：它不只是在浩瀚的文献中搜索答案，而是能够利用已有的数学公理和定理，发展出真正新颖的解题路径。
• 绝对的严谨性：每一个推理步骤都必须通过Lean的形式化验证，这彻底杜绝了大型语言模型常见的“幻觉”和逻辑谬误，保证了证明的绝对可靠。

谷歌的AlphaProof等系统也采用了类似思路，但Axiom的系统显然在技术上实现了新的突破。它不再是一个简单的计算器或搜索引擎，而是一个能够进行严密逻辑推理、甚至展现出某种“直觉”的思考者。

不止于数学：新范式的现实回响

这场发生在纯粹数学领域的革命，其影响力远不止于学术象牙塔。正如Axiom的CEO洪乐潼所说：“数学是现实世界最好的试验场和沙盒。”

Axiom正在探索的技术，有望在更广阔的领域产生巨大的商业价值。例如，在网络安全领域，同样的方法可以被用来开发更具韧性的软件。通过AI对代码进行形式化验证，可以从数学上确保其可靠与可信，抵御特定类型的网络攻击。在金融、物流优化、芯片设计等依赖复杂数学模型的行业，这种“AI数学家”同样潜力无限。

“计算器”还是“合作者”？重塑创新的边界

AI的崛起，再次引发了那个经典的问题：它会取代人类吗？

菲尔兹奖得主陶哲轩（Terence Tao）更愿意将AI视为一个“嵌入式助手”。他提出的“规格书”工作流——由人类设定目标、约束和验收标准，AI负责按步骤推进和验证——正在成为人机协作的新范式。在这种模式下，人类数学家的角色从繁重的计算和验证者，转变为更具创造性的**“战略规划师”和“问题提出者”**。

陈大卫的比喻或许最为贴切：“计算器发明后，数学家并没有忘记乘法表。”他相信，AI将扮演一个新颖的智能工具，或者更准确地说，一个**“智能伙伴”**的角色。

小野健则从AI身上看到了更深层的东西。他希望借助AxiomProver，去理解人类灵光一闪的“啊哈时刻”是否可以被预测，甚至从AI的证明过程中，反思自己过去的定理是如何被发现的。这不仅是对数学的探索，更是对创新本质的追问。

从悬置五年的猜想到一夜之间的证明，这不仅仅是一个数学难题的破解，更是一个新时代的序章。AI正从一个被动执行指令的工具，进化为一个能够主动探索、推理和创造的伙伴。它没有提供所有答案，但它无疑为人类智慧打开了更广阔、更深邃的地平线，而在这条地平线上，人与机器的协作，将是探索未知最激动人心的风景。