5年前，数学家陈大伟（Dawei Chen）和昆廷·让德龙（Quentin Gendron）在研究代数几何学中的微分问题时遇到瓶颈。他们的论证依赖于一个数论中的特殊公式，但始终无法完成证明。最终，他们只能将这个想法作为猜想发表。
上个月，在华盛顿特区的一场数学会议上，陈大伟遇到了著名数学家肯·小野（Ken Ono）。小野已从弗吉尼亚大学（University of Virginia）转投由其学生洪卡琳娜（Carina Hong）共同创立的人工智能公司Axiom。此前，陈大伟曾尝试使用ChatGPT寻求解决方案但未果。在与小野交流后，Axiom的人工智能系统AxiomProver迅速提供了完整的证明方案。
AxiomProver通过发现该问题与19世纪的一个数值现象之间的联系，成功构建并验证了证明。小野向《连线》杂志（WIRED）表示："AxiomProver发现了人类专家都未能察觉的关联。"
Axiom的系统近期已解决多个悬而未决的数学问题。虽然尚未攻克最著名的数学难题，但已证明了其在解决专业数学问题上的实力。该技术不仅限于纯数学领域，还可应用于开发更安全的软件系统，通过AI验证代码的可靠性。
Axiom采用将大型语言模型与专有的AxiomProver系统相结合的方法，并使用Lean数学语言进行证明验证。这使系统能够开发全新的解题方法，而不仅仅是检索已有文献。
其他重要成果包括解决费尔猜想（Fel's Conjecture），该猜想与印度数学家斯里尼瓦萨·拉马努金（Srinivasa Ramanujan）的研究相关。哈佛商学院教授斯科特·科米纳斯（Scott Kominers）评价这一成就"令人惊叹"。
陈大伟对AI在数学领域的应用持积极态度："就像计算器的发明并未使数学家遗忘乘法表一样，AI将作为智能伙伴，为数学研究开辟更广阔的视野。"
