Benjamin Skuse · 2026-03-03

人类与AI首次验证菲尔兹奖数学证明

摘要

2022年菲尔兹奖得主玛丽娜·维亚佐夫斯基关于高维球堆积的证明首次被人类与AI合作形式化验证。Math, Inc.开发的AI工具Gauss在5天内完成了8维证明，随后仅用两周时间完成了24维、超过20万行代码的证明。这一里程碑标志着自动形式化技术和人机协作在数学研究领域的重大突破。

内容框架与概述

文章首先介绍了维亚佐夫斯基本人在2016年解决的8维和24维球堆积问题，以及她因这项工作获得2022年菲尔兹奖的背景。接着描述了形式化验证项目的起源——一次偶然的相遇促成了本科生哈利哈兰与维亚佐夫斯基的合作，于2024年3月启动了Formalising Sphere Packing in Lean项目。随后重点阐述了Math, Inc.开发的AI工具Gauss如何加速这一进程，其新版本在2025年1月取得了突破性进展，不仅完成了8维证明的形式化，还发现了原论文中的一个笔误。最后，文章展望了这一技术进步对数学研究未来的深远意义。