2月5日，数学界的一个消息引起了轰动。一家名为Axiom(公理)的AI初创企业宣布，其开发的AI系统成功破解了四项此前未能解决的数学难题。这一突破不仅展示了人工智能日益增强的推理能力，也预示着科学发现的新范式。

　　故事要从5年前说起。数学家Dawei Chen和Quentin Gendron在研究代数几何中的微分问题时，被一个涉及数论的奇怪公式难住了。他们当时无法证明该公式，只能将其作为一项猜想发表。不久前，Dawei Chen尝试让ChatGPT来解决这个难题，但并未成功。转机出现在上个月华盛顿举行的一场数学会议上。Dawei Chen遇到了著名数学家Ken Ono。Ken Ono最近离开了弗吉尼亚大学的工作，加入了由他的学生Carina Hong创办的Axiom。

　　第二天早上，Ken Ono就带来了一个由公司开发的公理验证器生成的证明。Dawei Chen惊讶地发现，困扰多年的难题迎刃而解，目前这份证明已经发布在预印本平台上。公理验证器发现了一个19世纪就存在的数值现象与该问题之间的联系，并自主完成了验证。Ken Ono向《连线》杂志表示，这个证明发现了一些被人类数学家长期忽略的关键点。

　　这只是Axiom近期取得的一系列成就之一。虽然它尚未攻克那些举世闻名或奖金丰厚的顶级难题，但它解决了一些困扰专家多年的专业问题。Axiom的首席执行官Carina Hong解释说，他们的技术将大语言模型与专利系统相结合，通过一种名为Lean语言的专业数学语言进行逻辑推理和自动验证。这确保了AI生成的证明在逻辑上是无懈可击的。早在2024年，谷歌就通过阿尔法证明系统展示了类似的思路，而Carina Hong表示公理求解器在此基础上融入了更多先进技术。

　　另一个显著的突破是AI独立完成了费尔猜想的证明。费尔猜想涉及代数中的合系问题，其公式最早可以追溯到100多年前印度传奇数学家Srinivasa Ramanujan的笔记。哈佛商学院教授Scott Kominers对此感到震惊，他认为AI不仅实现了全自动解题，其产生的数学逻辑甚至具有某种优雅的美感。此外，AI还解决了数论中关于死胡同的概率模型，以及一个涉及费马大定理研究工具的难题。

　　除了纯数学研究，这种技术还具有极高的商业潜力。例如，AI验证代码逻辑的能力可以用于开发更安全的软件，防御网络安全攻击。正如Carina Hong所说，数学是检验现实世界的终极试验场。Dawei Chen则更加乐观，他认为AI并不是要取代数学家，而是像计算器一样，成为一种新型的智能合伙人，为人类开辟更广阔的研究视野。

（示意图）