全球 - 艾赫巴里通讯社
里程碑时刻：AI与人类合作正式验证菲尔兹奖数学证明
数学界最近见证了一项前所未有的成就，标志着人工智能与人类智慧合作的一个真正转折点。由新兴初创公司Math, Inc.开发的名为Gauss的AI系统，已成功并正式验证了乌克兰数学家玛丽娜·维亚佐夫斯卡（Maryna Viazovska）关于8维和24维空间中球体最优堆积问题的复杂菲尔兹奖获奖数学证明。这一开创性成就不仅证实了维亚佐夫斯卡深奥工作的深刻有效性，也为AI增强的数学研究的未来开辟了广阔的新视野。
玛丽娜·维亚佐夫斯卡于2022年7月获得了享有盛誉的菲尔兹奖（通常被认为是数学界的诺贝尔奖），她不仅是该奖项86年历史上第二位女性获奖者，而且在她国家被入侵仅仅几个月后就获得了这一荣誉，因此受到了全球关注。维亚佐夫斯卡以其在球体堆积问题上的开创性工作而闻名，这个问题基本探究的是：在n维空间中，相同的圆形、球体或超球体能被多密集地排列？2016年，她利用强大的数学函数（称为准模形式）为8维和24维空间的问题提供了优雅的解决方案。她证明了被称为E8的对称排列在8维中是最佳的，并与合作者一起证明了Leach格在24维中是最佳的。虽然这些结果可能看起来抽象，但它们具有重要的实际意义，包括改进智能手机和太空探测器中使用的纠错码。
另请阅读
维亚佐夫斯卡的证明此前已由传统数学界严格验证，从而获得了菲尔兹奖的认可。然而，“形式化验证”——即证明能够通过计算机进行绝对正确性验证的能力——代表着完全不同水平的精确性和严谨性。普林斯顿大学AI推理专家和博士后利亚姆·福尔（Liam Fowl）将形式化验证比作一个“橡皮图章”或“真实认证”，它确保了推理陈述的绝对正确性。在过去几年中，特别是自2022年以来，AI辅助形式化证明验证方面取得了实质性进展。
这项变革性项目的起源始于维亚佐夫斯卡与西达斯·哈里哈兰（Sidharth Hariharan）在瑞士洛桑的一次偶然会面，当时哈里哈兰还是一名大三学生，但已精通证明的形式化。维亚佐夫斯卡出于好奇表达了将其工作形式化的兴趣，这促成了2024年3月“Lean中的球体堆积形式化”项目的诞生。Lean是一种流行的编程语言和“证明助手”，它使数学家能够构建证明，然后由计算机系统对其绝对正确性进行验证。
这项合作工作涉及巴维克·梅塔（Bhavik Mehta）、克里斯托弗·伯克贝克（Christopher Birkbeck）和李世宇（Seewoo Lee）等专家，最初的重点是创建一个人类可读的“蓝图”，以映射8维证明的组成部分，并确定哪些元素仍需要形式化。经过大约15个月的开发，该项目的存储库于2025年6月向公众开放。到10月下旬，Math, Inc.登场，推出了他们的AI系统Gauss。Math, Inc.的首席执行官兼联合创始人杰西·韩（Jesse Han）将Gauss描述为一个复杂的“推理代理”，它无缝地整合了自然语言推理和完全形式化推理，能够进行文献搜索、利用工具并生成Lean代码进行验证。
Gauss已经建立了强大的声誉，它在短短三周内完成了强素数定理（PNT）的Lean形式化——这项任务曾让菲尔兹奖得主们投入精力。在与哈里哈兰团队的首次互动中，Gauss证明了30个“sorrys”（团队寻求验证的中间事实），甚至帮助识别并纠正了他们项目中的一个错误。然而，随后经历了一段“无线电静默”。哈里哈兰和他的同事们并不知道，Math, Inc.正忙于开发一个显著更强大的Gauss版本，并在1月中旬取得了研究突破，使新系统能够在短短两到三天内重现PNT形式化。
几天后，增强版的Gauss被重新定向到球体堆积形式化任务。利用哈里哈兰团队提供的宝贵现有蓝图和共享工作，Gauss不仅自动形式化了整个8维案例，还在五天内独立发现并纠正了已发表论文中的一个错误。更令人惊叹的是，Math, Inc.现在透露了另一项壮举：Gauss在极短的时间内自动形式化了维亚佐夫斯卡24维球体堆积的证明——包括超过20万行代码。哈里哈兰表达了他的惊讶和兴奋，强调这项技术有潜力“做伟大的事情，并以非凡的方式帮助数学家”。
相关新闻
这一发展标志着数学研究方式的深刻转变，AI正在演变为发现之旅中不可或缺的伙伴。它有望加速复杂证明的验证速度，使人类数学家能够专注于概念创新，并为更深入地理解数学宇宙打开大门。
