数学中人工智能与人类协作的里程碑时刻

乌克兰数学家Maryna Viazovska关于最优球体堆积的菲尔兹奖获奖证明，现已通过人类与人工智能的协作完成了形式化验证，这标志着人工智能在数学研究中发挥作用取得了重大进展。

Viazovska的原始工作解决了8维（使用E8排列）和24维（使用Leech晶格）的球体堆积问题，并已获得数学界的认可。然而，形式化验证——即确保证明可以通过计算机使用如Lean这样的证明助手进行检查——是一个不同的挑战。在本科生Sidharth Hariharan与Viazovska取得联系后，旨在形式化其证明的“在Lean中形式化球体堆积”项目启动。

当开发名为Gauss的人工智能推理代理的初创公司Math, Inc.介入后，合作显著加速。Gauss首先为8维情况证明了30个中间事实（“sorry”）。随后，一个改进版的Gauss在五天内自动完成了整个8维证明的形式化，甚至发现了并修正了已发表论文中的一个拼写错误。接着，Gauss仅用两周时间就自动形式化了更复杂的24维证明，其中涉及超过20万行代码，并利用了8维案例中建立的基础理论。人类合作者和AI开发者都认为这是一个革命性的进步，预示着此类技术将使数学家能够专注于概念上的发现。

(来源：ieeespectrum)