AI智能体用24天检查完数学史上最长的证明

初创公司Axiom Math周一发布了有限单群分类定理的计算机验证证明。数十个AI智能体用Lean写了约4300万行代码，Lean是一种能检查证明的语言。这项工作发现了已发表证明中的34处重要缺口，Axiom请专家重新核查结果。

为什么重要?原始证明约有1.5万页，出自约100位数学家之手，一个人几乎无法重新核查。如今机器几周就能审查这样的巨型成果，数学家信任结论的方式也会随之改变。

相关新闻