一个新的人工智能数学初创公司刚刚解决了4个先前未解决的问题

📢 转载信息

原文链接：https://www.wired.com/story/a-new-ai-math-ai-startup-just-cracked-4-previously-unsolved-problems/

原文作者：Will Knight

---

五年前，数学家陈大卫（Dawei Chen）和昆汀·让德龙（Quentin Gendron）正试图梳理代数几何中一个涉及微分的难题，微分是微积分中用于测量沿弯曲表面距离的元素。在研究一个定理时，他们遇到了一个意想不到的障碍：他们的论证依赖于数论中一个奇怪的公式，但他们无法解出或证明这个公式。最终，陈和让德龙撰写了一篇论文，将他们的想法作为一种猜想而不是定理提出了。

陈最近花了好几个小时向ChatGPT提问，希望能让AI想出解决这个尚未解决的问题的方法，但收效甚微。然后，在上个月于华盛顿特区举行的一次数学会议招待会上，陈遇到了著名的数学家小野贤（Ken Ono）。小野贤最近辞去了弗吉尼亚大学的工作，加入了Axiom，这是一家由他的门生卡琳娜·洪（Carina Hong）共同创立的人工智能初创公司。

陈向小野先生讲述了这个问题，第二天早上，小野先生拿出了一个证明，这是他公司解决数学问题的AI——AxiomProver提供的。“之后一切都很自然地迎刃而解了，”陈说。他与Axiom合作整理了这份证明，该证明现已发布在arXiv上，这是一个学术论文的公开存储库。

Axiom的AI工具找到了这个问题与19世纪首次研究的一种数值现象之间的联系。然后它设计了一个证明，并很有用地进行了自我验证。小野先生告诉WIRED：“AxiomProver发现的东西是所有人类都忽略了的。”

这份证明是Axiom声称其系统在最近几周提出的几项未解数学问题解决方案之一。该AI尚未解决该领域最著名（或最有价值）的问题，但它已经找到了困扰不同领域专家多年的问题的答案。这些证明是AI数学能力稳步发展的证据。最近几个月，其他数学家也报告说使用AI工具来探索新想法和解决现有问题。

Axiom正在开发的技术可能在高等数学世界之外也证明有用。例如，采用相同的方法可以开发出对某些类型的网络安全攻击更具弹性的软件。这需要利用AI来验证代码是可证明可靠和值得信赖的。

Axiom的首席执行官洪女士说：“数学是检验现实的绝佳试验场和沙盒。我们相信，在具有高商业价值的领域中存在许多相当重要的用例。”

Axiom的方法涉及将大型语言模型与一个名为AxiomProver的专有AI系统相结合，该系统经过训练，可以推理数学问题以得出可证明正确的解决方案。2024年，谷歌用一个名为AlphaProof的系统演示了类似的想法。洪女士表示，AxiomSolver融入了多项重大进展和更新的技术。

小野先生说，AxiomProver生成的陈-让德龙猜想的AI证明展示了AI如何能够有意义地协助专业数学家。“这是一种证明定理的新范式，”他说。

Axiom的系统不仅仅是一个常规的AI模型，因为它能够使用一种称为Lean的专业数学语言来验证证明。这使得AxiomProver能够开发出真正新颖的解题方法，而不仅仅是在文献中搜索。

AxiomProver生成的另一个新证明展示了AI完全独立解决数学问题的能力。该证明也发布在arXiv上，为Fel’s Conjecture（费尔猜想）提供了解决方案，该猜想涉及代数中的“列对齐”现象，即数学表达式中的syzygies。值得注意的是，该猜想涉及传奇印度数学家斯里尼瓦萨·拉马努金（Srinivasa Ramanujan）一百多年前在笔记本中发现的公式。在这种情况下，AxiomProver不仅仅是填补了一个缺失的环节，而是从头到尾设计了证明。