北京
新智元报道
编辑：倾倾
【新智元导读】2026数学界直接寄了！顶尖学者未能推进的证明被跑通，连菲尔兹奖得主也被指出论文逻辑瑕疵。当AI智能体能自主接管真理的验证权时，现有的科研范式还能维持多久？
太离谱了！数学界被AI Gauss洗劫了。
仅5天，它就啃完了人类15月都啃不动的硬骨头。
Viazovska 8维+24维球填充证明，硬转成20万行Lean代码，90倍效率碾压！
人类精英 VS AI？纯属算盘怼量子，根本打不过。
网友吐槽：救命，这AI卷疯了，DeepMind都得认怂？
Gauss给菲尔兹奖主发「纠错邮件」
8维和24维的证明针对的是球体堆积问题。
在n维欧几里得空间中，如何将相同大小的球（无重叠）尽可能密集地排列，并证明特定格子达到最优。
这个问题已有数百年历史。在大多数维度难以严格证明最优，但8维和24维是特殊维度。
2022 Viazovska靠8维E8+24维Leech晶格球填充爆杀全场，成第二位女菲奖得主。
论文传送门：http://arxiv.org/abs/1603.04246
论文传送门：https://arxiv.org/abs/1603.06518
但现在，AI卷上来了！
Viazovska的论文有几十页，人类逻辑压缩成自然语。
但电脑眼里，「理应如此」这种词根本不能理解。
在Gauss介入之前，一个团队耗时15个月，试图将这一菲尔兹奖成果进行Lean形式化。
但受制于人类认知带宽的限制与注意力衰减，工程推进缓慢。
从15个月到5天，人类处理超大规模逻辑链条的算力已经触达上限。
8维证明形式化：AI狠戳菲奖论文瑕疵
Gauss底层是推理智能体闭环，碾压老代码。检索模块狂扫千篇文献补背景，重构模块直转Lean代码+实时编译验证。
处理Viazovska 8维E8模系数时，Gauss发现了30个逻辑瑕疵。
在Lean社区中，这些尚未被机器验证的步骤通常被标注为「sorry」。
而对于人类开发者而言，填补这些「sorry」意味着需要查阅巨量的文献，并将其翻译成机器能识别的语法。
转折点出现在论文第14页的一处不等式推导。
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
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
