AI用于验证迄今最难的数学证明

Axiom Math公司使用其AI系统AxiomProver，首次自动验证了与素数相关的“246定理”的证明，标志着AI辅助数学研究的重要里程碑。

• AxiomProver是自主多智能体系统，能将数学陈述转化为机器可检查的证明。
• 此次验证的“246定理”是素数间隙研究中的旗舰结果，代表了人类关于素数知识的当前阈值。
• 形式化验证并非100%保证正确，曾演示过利用方法中的bug可让假的AI生成证明被接受。
• Axiom Math今年已用该系统解决数个未解数学问题，并验证了更多证明。
• 竞争对手Math Inc早前用Gauss agent形式化了Viazovska的球堆积证明，但业内人士认为246定理的形式化更全面、更有用。

• Representing a significant milestone in AI-assisted mathematical research, a team at Axiom Math has automatically verified the proof of a theorem relating to prime numbers—colloquially referred to as the “246 theorem”—for the first time using the company’s AI system AxiomProver.
• The process is not a 100 percent guarantee that the proof is correct, as a recent demonstration showed , exposing how a bug in the method could be exploited to accept a false, AI-generated proof.
• “This theorem currently represents the threshold of human knowledge about prime numbers.”