Claude用Lean严格验证，攻克菲尔兹奖得主数年未解的渗流猜想

2026年8月30日，菲尔兹奖得主Hugo Duminil-Copin发文感叹，他倾注数年心血、屡败屡战的渗流猜想，恐怕迟早会被AI攻克。几乎同时，同行在GitHub上发现Anthropic工程师提交的代码仓库，其中是由大语言模型Claude生成、并经Lean严格验证的完整证明——困扰人类近70年的连续相变猜想已被AI证明。没有发布会，没有官方博客，消息传出后全球数学界震动。德国数学家Benedikt Jahnel表示，若由人类证明，大概率能拿菲尔兹奖，但这次是AI跨过终点。Gil Kalai也称，若获验证，将是非凡突破。

渗流理论中的连续相变猜想被称为概率论“圣杯”。1957年，Broadbent和Hammersley提出：液体如何穿过多孔海绵？可想象为网格管道，每根以概率p畅通、1-p堵塞。p很小时水无法穿透，p很大时形成无限连通网络，中间存在临界概率，类似水结冰的相变。高维（11维及以上）已被证明相变连续，但3到10维因缺乏二维对称性、又无法套用高维均场工具，成为数十年无法逾越的“叹息之墙”。

Duminil-Copin是“撞墙者”中最著名的一位。2022年他因统计物理相变领域工作获菲尔兹奖，学术生涯几乎与渗流理论纠缠。他在博客中写道，数学问题不仅是待证定理，更是灵魂导师；自己多次攻克3到10维连续相变失败，但失败草稿孕育了数十个灵感，日后获奖工作多是这道主线任务失败后的“副产物”。然而Anthropic的入局撕碎了这种浪漫。提交证明的Justin Leder并非数学泰斗，依托的是尚未公开的超前代Claude模型。AI不体会迷茫与审美，用形式化逻辑一路平推。Jahnel坦言感情复杂：高兴猜想被证明，又因AI踢出临门一脚而失落幻灭。

AI并非暴力穷举。2024年，Gady Kozma与Shahaf Nitzan发表开创性论文，将终点拉近到只差求证一个不等式，但该不等式总在关键节点奇异崩溃。Anthropic模型抓住这一跳板，在Lean约束下调用已知分析工具与不等式技巧，以人类未设想的精巧路径，构筑数千行推理闭环，将其证明。宾夕法尼亚大学数学家Ahmed Bou-Rabee宣布该证明，并借助大模型仅一天就对代码进行泛化和修改。他感慨，AI让他做到以前不敢想的事，有些项目苦做八年无进展，如今距彻底解决仅一步之遥。但Kozma教授保持克制，称暂不置评，仍在等待Anthropic发布“人类能看懂的版本”。

蒸汽机、照相机、深蓝、AlphaGo都曾引发“终结”哀叹，但围棋未死，人类棋手借AI看到全新定式。数学亦然。Duminil-Copin认为，证明定理从不是数学全部，猜想魅力在于攻克时孕育的工具革命：费马大定理催生代数几何，黎曼猜想推动解析数论。他数年攻坚失败，却催生几十个新想法，带来意外发现。未来数学家或许不再消耗于数十年繁复推导，而是挑选探索航线、指挥推理智能体、阐释机器带回的智慧碎片。从1957年海绵吸水猜想，到2026年被AI在GitHub上证明，人类用70年见证智慧形态的交接。