新智元报道
数学界迎来了一场前所未有的变革，顶尖数学家难以推进的证明问题被AI解决了，连菲尔兹奖得主也不可避免地受到了质疑。
AI在数学领域引发了一场风暴，它对传统研究方式构成了挑战。
在短短五天内，AI就完成了人类历时十五个月才能完成的工作。
Viazovska提出的关于8维和24维球填充问题的证明被转换成近二十万行Lean代码，效率惊人地提升了九十多倍。
人类智慧与AI技术之间的较量似乎已经分出了胜负，人类难以匹敌强大的计算能力。
网络上对此议论纷纷：有人惊呼“救命”，有人感叹DeepMind也自愧不如。
AI Gauss向菲尔兹奖得主发送了纠错邮件。
证明的焦点集中在球体堆积问题上，即如何在n维欧几里得空间中以最紧密的方式排列相同大小的球体，并确定最优排列方式的具体格子结构。
这个数学难题已有数百年历史，在大多数维度下难以得到严格的证明，但8维和24维是例外的情况。
2022年，Viazovska在8维E8和24维Leech晶格球填充问题上取得了突破性进展，并因此成为第二位女性菲尔兹奖得主。
在她发表的论文中，提出了关于如何优化高维度空间内球体排列的具体方法。
AI系统将人类难以理解的高度抽象理论转化为机器可执行的形式化代码。
由于复杂的逻辑推理和庞大的数据量，在没有AI介入的情况下，这项工作几乎无法在短时间内完成。
AI Gauss的出现让这一过程变得高效而精确。
在处理Viazovska论文的过程中，Gauss发现了三十个潜在错误，并修正了它们。
这些问题通常被标记为“遗憾”，意味着需要进一步验证或补充证明。
令人惊讶的是，在无需人工干预的情况下，AI系统独立完成了这一任务。
AI的推理能力超越了人类的认知极限，展现出更敏锐的纠错直觉。
在数学界看来，将复杂理论转化为可执行代码是一个重要的里程碑。
Gauss通过其强大的检索和重构模块，在没有现有蓝图的情况下自主完成了24维球填充问题的证明工作。
它不仅能够识别并修复人类逻辑中的盲点，还能自行生成数万行Lean代码进行验证。
这种能力标志着数学理论从自然语言论文向可运行软件工程的转变。
Math,Inc.首席执行官Jesse Han将这一变化比作计算机科学从早期的手动打孔纸带编程过渡到高级语言时代的飞跃。
随着技术的进步，未来的数学证明工作或将由类似Gauss这样的推理智能体自动完成，而人类则专注于更抽象的理论设计与创新。
这种新的范式不仅解放了数学家的时间和精力，还加速了许多科学领域的研究进程。
Gauss在连续执行4096次推理步进后，反馈了编译错误，并指向了原论文中的一处排版与微观逻辑瑕疵。
在没有人类干预的情况下，Gauss通过自主搜寻历史定理库，重构了这一步的边界条件，并补全了这段缺失的证明。
在此之前，人类数学家始终作为逻辑的主理人，AI仅负责执行；而现在，Gauss展现出了比人类更敏锐的纠错直觉。
对于学界而言，8维证明的完全形式化本身就是一个分水岭。
它不仅产出了数万行高质量的Lean代码，更证明了推理智能体具备识别并修复人类逻辑盲点的能力。
这种能力将数学验证从模糊地带，推向了100%可运行的数字绝对值。
24维证明：零蓝图自主重构
在数学界，24维空间的Leech Lattice远比8维的E8晶格复杂。
Gauss这一次没有任何预设的蓝图可以参考，其复杂程度显著高于8维情况。
在8维证明的形式化过程中，人类团队已经提前在Lean社区搭建了脚手架，标注了大量的「sorry」作为导向。
但在24维证明中，Gauss面对的是一片逻辑真空。
24维球体填充证明的难点在于，它深度耦合了关于Leech晶格唯一性的复杂群论证明。
Gauss展现出的核心突破是无蓝图推理。
在证明Leech晶格是24维空间中唯一能够实现最大密度的结构时，Gauss表现出了超强的文献综合能力。
论文传送门：https://arxiv.org/abs/2601.04567
系统通过其检索模块，定位了数十篇跨越30年的关联论文。
它理解了Viazovska原始论文的逻辑主线，通过跨文献比对，自行识别出需要引入的外部引理，例如关于Co0康威群的对称性特征。
在24维证明的深度推进中，Gauss需要生成并验证超过12万行的Lean代码。
在这一规模下，任何由于上下文理解偏差导致的逻辑漂移，都会引发指数级的报错崩溃。
Gauss通过推理链条都监控，实时计算每一个推论步骤的置信度。当置信度低于阈值时，它会触发回溯机制，重新检索数学公理库。
在24维证明的第2048个逻辑块中，Gauss独立补全了拉普拉斯算子在特定流形上的谱隙估计。
这一步在原论文中被视为「显而易见」的结论，但在形式化验证中，它需要近万行的证明代码。
Gauss仅用14小时就完成了这段逻辑的填补。AI对高难度智力活动的重塑，变成了全流程科研链条的自主接管。
在逻辑验证的竞技场上，人类已经不再不可或缺。
范式转移：数学证明的工程化纪元
长期以来，数学证明的传播媒介是自然语言论文。这种媒介形式虽然灵活，却伴随着极高的理解门槛与逻辑验证成本。
Gauss的出现，标志着数学正从自然语言文学转向可运行的软件工程。
Math,Inc.首席执行官Jesse Han将这一转变比作计算机科学从打孔纸带时代进入高级语言时代。
在打孔纸带时代，程序员需要关注每一个底层的物理比特；而在高级语言时代，开发者得以站在抽象层级上构思复杂的系统逻辑。
Jesse Han认为：
这种技术的最终结果将是解放数学家……让他们去梦想新的数学世界。
未来数学家将转向更高的架构设计，数学证明等工作将由类似Gauss的推理智能体自动完成。
数学作为所有自然科学的底层语言，其工程化进度的加快，将直接传导至密码学、量子计算、航天轨道计算等强逻辑领域。
在这种新范式下，人类将作为指挥家，繁重的演绎推理则交给具备ASI潜力的智能体。
Maryna Viazovska曾被视为人类智力的巅峰，如今它已转化为服务器中202000行的比特。
在这个真理不再需要人类中介的时代，我们是否有勇气沿着AI开辟的路径，去触碰那些超越人类直觉的未知疆域？
参考资料：
https://spectrum.ieee.org/ai-proof-verification?share_id=9202657&utm_campaign=RebelMouse&utm_content=IEEE+Spectrum&utm_medium=social&utm_source=twitter
https://x.com/mathematics_inc/status/2028542388717986135?s=20