内容来源：https://www.wired.com/story/a-new-ai-math-ai-startup-just-cracked-4-previously-unsolved-problems/

内容总结：

近日，人工智能在数学研究领域取得突破性进展。一家名为Axiom的初创公司研发的AI系统AxiomProver，成功解决了多个困扰数学家多年的难题，其中包括五年前由数学家陈大卫（Dawei Chen）和昆汀·詹德隆（Quentin Gendron）提出的“陈-詹德隆猜想”。

该猜想源于代数几何中一个涉及微分形式的复杂问题。两位数学家曾因一个数论公式无法论证，只能将成果以猜想形式发表。上月，陈大卫在华盛顿特区的一次数学会议上偶遇知名数学家小野健（Ken Ono，现任Axiom公司顾问），随后AxiomProver在一夜之间为该猜想提供了完整证明。该证明已发表于预印本平台arXiv。

AxiomProver的核心能力在于将大语言模型与专为数学推理设计的验证系统相结合，不仅能自主推导证明，还能通过形式化验证工具Lean确保论证严密性。除上述猜想外，该系统还独立证明了涉及印度传奇数学家拉马努金笔记的“费尔猜想”，以及数论中关于“死胡同”概率模型的难题，甚至借鉴了攻克费马大定理的数学工具。

哈佛商学院教授斯科特·科米纳斯评价称，AI不仅实现了全自动化解题与即时验证，其生成的数学证明更展现出“优雅之美”。Axiom首席执行官卡丽娜·洪指出，该技术不仅是数学研究的“试验场”，未来还可应用于开发抗网络攻击的可靠软件，具有重要商业价值。

数学家们普遍认为，AI正在成为数学研究的新型智能伙伴。正如陈大卫所言：“计算器没有让数学家忘记乘法表，AI也将为数学研究开辟更广阔的前景。”这一系列成果标志着人工智能正在推动数学研究进入新范式。

中文翻译：

五年前，数学家陈大卫和昆汀·詹德隆正试图攻克代数几何中一个涉及微分的复杂领域——微分是用于测量曲面距离的微积分元素。在研究某个定理时，他们意外遭遇了障碍：其论证依赖于数论中一个奇特的公式，但他们既无法求解也无法证明其合理性。最终，陈和詹德隆将这一构想以猜想而非定理的形式写成论文发表。

近期，陈大卫花费数小时反复向ChatGPT提问，希望这个人工智能能为这个悬而未决的难题提供解决方案，但始终未果。直到上个月在华盛顿特区的一场数学会议招待会上，他偶遇了知名数学家小野健。小野健不久前刚从弗吉尼亚大学离职，加入了由他的门生卡丽娜·洪共同创立的人工智能初创公司Axiom。

陈向小野健描述了该问题。次日上午，小野健借助其初创公司的数学求解人工智能系统AxiomProver，向陈展示了一份证明。"此后一切豁然开朗，"陈大卫表示。他与Axiom团队合作撰写了证明论文，现已发布在学术论文公共存储库arXiv上。

Axiom的人工智能工具发现了该问题与19世纪首次研究的某种数值现象之间的关联，随后设计并自行验证了证明过程。"AxiomProver的发现揭示了所有人类研究者都忽略的线索，"小野健在接受《连线》采访时表示。

这份证明是Axiom宣称其系统近几周解决的多个数学难题之一。虽然该系统尚未破解数学领域任何最著名（或最具经济价值）的难题，但已为困扰不同领域专家多年的问题找到了答案。这些证明标志着人工智能数学能力的稳步提升。近几个月来，已有其他数学家报告使用AI工具探索新思路并解决现有问题。

Axiom开发的技术可能在高等数学领域之外产生价值。例如，相同方法可用于开发更能抵御特定类型网络攻击的软件，即通过人工智能验证代码的可证明可靠性与可信度。

"数学本质上是现实的终极试验场与沙盒，"Axiom首席执行官卡丽娜·洪表示，"我们确信这项技术蕴含着大量具有高商业价值的重要应用场景。"

Axiom的技术路径将大型语言模型与专有人工智能系统AxiomProver相结合，后者经过专门训练，可通过逻辑推理解决数学问题，并确保解决方案的可证明正确性。2024年，谷歌的AlphaProof系统曾展示过类似理念。洪指出，AxiomSolver系统融合了多项重大改进与新兴技术。

小野健认为，针对陈-詹德隆猜想的人工智能证明，展现了AI如今如何实质性地协助专业数学家工作。"这标志着定理证明的新范式，"他表示。

Axiom系统超越常规AI模型之处在于，它能使用名为Lean的专用数学语言验证证明。这使得AxiomProver不仅能检索文献，更能开创真正新颖的问题解决路径。

AxiomProver生成的另一项新证明，展示了该系统完全独立解决数学问题的能力。这份同样发布于arXiv的论文，解决了涉及代数齐次关系的费尔猜想。值得注意的是，该猜想涉及的公式最早出现在百年前传奇印度数学家斯里尼瓦瑟·拉马努金的笔记中。此次AxiomProver不仅填补了缺失环节，更完成了从零构建完整证明的壮举。

"即便作为持续关注AI数学工具发展多年并亲身实践的研究者，我仍对此感到震惊，"哈佛商学院教授斯科特·科米纳斯评价道。他既熟悉费尔猜想，也了解Axiom的技术。"AxiomProver不仅能全自动解决此类问题并即时验证——这本身已令人惊叹——其生成的数学证明更展现出优雅的美感。"

Axiom人工智能生成的第三项证明涉及数论中"死胡同"概念的概率模型。第四项证明则借鉴了最初为攻克费马大定理而开发的数学工具——该定理是数学史上最著名的挑战之一。

小野健希望AxiomProver不仅能辅助数学家工作，更能揭示科学发现机制的深层规律。"我试图探究能否使'灵光乍现'的时刻变得可预测，"他表示，"这个过程也让我重新审视了自己某些定理的证明方式。"

亲眼见证猜想被解决的陈大卫，对AI给数学领域带来的影响持乐观态度："计算器发明后，数学家并未忘记乘法表。我相信AI将成为一种新颖的智能工具——或许'智能伙伴'更为贴切——为数学研究开启更丰富广阔的视野。"

本文节选自威尔·奈特《AI实验室》通讯专栏，过往内容可通过此处查阅。

英文来源：

Five years ago, mathematicians Dawei Chen and Quentin Gendron were trying to untangle a difficult area of algebraic geometry involving differentials, elements of calculus used to measure distance along curved surfaces. While working on one theorem, they ran into an unexpected roadblock: Their argument depended on a strange formula from number theory, but they were unable to solve or justify it. In the end, Chen and Gendron wrote a paper presenting their idea as a conjecture, rather than a theorem.
Chen recently spent hours prompting ChatGPT in the hopes of getting the AI to come up with a solution to the still unsolved problem, but it wasn’t working. Then, during a reception at a math conference in Washington, DC, last month, Chen ran into Ken Ono, a well-known mathematician who had recently left his job at the University of Virginia to join Axiom, an artificial intelligence startup cofounded by one of his mentees, Carina Hong.
Chen told Ono about the problem, and the following morning, Ono presented him with a proof, courtesy of his startup’s math-solving AI, AxiomProver. “Everything fell into place naturally after that,” says Chen, who worked with Axiom to write up the proof, which has now been posted to arXiv, a public repository for academic papers.
Axiom’s AI tool found a connection between the problem and a numerical phenomenon first studied in the 19th century. It then devised a proof, which it helpfully verified itself. “What AxiomProver found was something that all the humans had missed,” Ono tells WIRED.
The proof is one of several solutions to unsolved math problems that Axiom says its system has come up with in recent weeks. The AI has not yet solved any of the most famous (or lucrative) problems in the field of mathematics, but it has found answers to questions that have stumped experts in different areas for years. The proofs are evidence of AI’s steadily advancing math abilities. In recent months, other mathematicians have reported using AI tools to explore new ideas and solve existing problems.
The techniques being developed by Axiom may prove useful outside the world of advanced math. For example, the same approaches could be used to develop software that is more resilient to certain kinds of cybersecurity attacks. This would involve using AI to verify that code is provably reliable and trustworthy.
“Math is really the great test ground and sandbox for reality,” says Hong, Axiom’s CEO. “We do believe that there are a lot of pretty important use cases of high commercial value.”
Axiom’s approach involves combining large language models with a proprietary AI system called AxiomProver that is trained to reason through math problems to reach solutions that are provably correct. In 2024, Google demonstrated a similar idea with a system called AlphaProof. Hong says that AxiomSolver incorporates several significant advances and newer techniques.
Ono says the AI-generated proof for the Chen-Gendron conjecture shows how AI can now meaningfully assist professional mathematicians. “This is a new paradigm for proving theorems,” he says.
Axiom’s system is more than just a regular AI model, in that it is able to verify proofs using a specialized mathematical language called Lean. Rather than just search through the literature, this allows AxiomProver to develop genuinely novel ways of solving problems.
Another one of the new proofs generated by AxiomProver demonstrates how the AI is capable of solving math problems entirely on its own. That proof, which has also been described in a paper posted to arXiv, provides a solution to Fel’s Conjecture, which concerns syzygies, or mathematical expressions where numbers line up in algebra. Remarkably, the conjecture involves formulas first found in the notebook of legendary Indian mathematician Srinivasa Ramanujan more than 100 years ago. In this case AxiomProver did not just fill in a missing piece of the puzzle, it devised the proof from start to finish.
“Even as someone who's been watching the evolution of AI math tools closely for years, and working with them myself, I find this pretty astounding,” says Scott Kominers, a professor at Harvard Business School who is familiar with Fel’s conjecture as well as with Axiom’s technology. “It's not just that AxiomProver managed to solve a problem like this fully automated, and instantly verified, which on its own is amazing, but also the elegance and beauty of the math it produced.”
The third proof generated by Axiom’s AI involves a probabilistic model of so-called “dead ends” in number theory. The fourth draws on mathematical tools originally developed to attack and ultimately solve Fermat’s Last Theorem, one of the field’s most famous challenges.
Ono says he hopes that AxiomProver will not only assist mathematicians with their work, but also reveal something more fundamental about how new discoveries are made. “I’m interested in trying to understand if you can make these aha moments predictable,” he says. “And I’m learning a lot about how I proved some of my own theorems.”
Chen, who witnessed his own conjecture solved by Axiom recently, says he is also feeling optimistic about the impact AI will have on his field. “Mathematicians did not forget multiplication tables after the invention of the calculator,” Chen says. “I believe AI will serve as a novel intelligent tool—or perhaps an ‘intelligent partner’ is more apt—opening up richer and broader horizons for mathematical research.”
This is an edition of Will Knight’s AI Lab newsletter. Read previous newsletters here.