主要内容
五年前，数学家陈大为与Quentin Gendron在代数几何研究中遇到一个难题：其猜想依赖数论中的一个未解决公式，无法证明。近日，在华盛顿数学会议上，陈借助AI公司Axiom的数学求解系统“AxiomProver”，由数学家Ken Ono验证了该猜想的证明，成果已发布至arXiv预印本平台。
陈称：“证明过程自然衔接。”AxiomProver发现问题与19世纪首次研究的数值现象相关，进而自行构建并验证了证明。“AI找到了人类忽略的关键连接。”Ono表示。
Axiom近期公布的证明显示，其系统已攻克多个学界难题：除上述猜想外，还独立解决了涉及印度数学家拉马努金100多年前笔记公式的Fel’s Conjecture（合冲问题）。尽管尚未解决黎曼猜想等“最著名数学难题”，但AI已展现出攻克长期悬而未决问题的能力。
Axiom结合大语言模型与AxiomProver（采用数学语言Lean验证证明），其技术或可应用于网络安全（如验证代码可靠性）。这一进展标志着AI在数学推理能力上的突破，或为跨学科研究提供新范式。