详细内容或原文请订阅后点击阅览
Maryna Viazovska 使用 AI 形式化的球堆积证明
玛丽娜·维亚佐夫斯卡。图片来源：EPFL 2026。为 EPFL 教授 Maryna Viazovska 赢得 2022 年菲尔兹奖的证明达到了一个新的里程碑：通过数学家和人工智能工具之间的合作，通过计算机完成了它们的形式化。 2016 年，Maryna Viazovska 解决了 8 维球体堆积问题，证明了 E₈ 晶格 [...]
来源:ΑΙhub玛丽娜·维亚佐夫斯卡。图片来源：EPFL 2026。
为 EPFL 教授 Maryna Viazovska 赢得 2022 年菲尔兹奖的证明达到了一个新的里程碑：通过数学家和人工智能工具之间的合作，通过计算机完成了它们的形式化。
2016年，Maryna Viazovska解决了8维球体堆积问题，证明E₈晶格构成了最稠密的排列。不久之后，她与合作者一起使用 Leech 晶格在 24 维上建立了类似的结果。她的方法为研究了几个世纪的问题提供了一个优雅的解决方案，与纠错码等应用领域密切相关。
由于这一重大贡献，维亚佐夫斯卡于 2022 年被授予菲尔兹奖，这是数学界的最高荣誉。她的证明很快被科学界接受，但通过计算机正式验证它代表着另一种挑战：它需要将推理的每一步翻译成软件可以自动检查的逻辑语言。
Viazovska 和年轻数学家 Sidharth Hariharan 在洛桑举行会议后于 2024 年启动了“精益形式化球堆积”项目，该项目承担了这项任务。该团队与几位国际研究人员合作，构建了 8 维证明的详细蓝图，并逐步将其转化为数学中广泛使用的证明助手 Lean。由初创公司 Math, Inc. 开发的专业人工智能高斯在形式化过程中发挥了决定性作用。通过帮助完成某些中间步骤，它加快了流程，使 8 维案例能够在五天内完成，随后两周内完成相当大的 24 维案例（超过 200,000 行代码）。
了解更多
人工智能与人类数学合作的分水岭时刻——二十一世纪菲尔兹奖证明首次正式化，IEEE Spectrum。
洛桑联邦理工学院