10月2日前后，北京大学AI for Math团队宣布一项标志性进展：已在Lean 4证明助手中完整形式化庞加莱猜想，并推出首个通过双检验的版本。团队利用公开可用的商用大模型，在不到半个月时间里生成约320万行代码，总成本不到3万美元。几乎同一时间，一个美国团队也提交了约470万行的独立Lean证明。同一场百年数学难题，两支团队先后交出机器可验证的完整形式化成果，这在全球AI数学领域尚属首次。
先说清概念。庞加莱猜想是拓扑学的著名难题，问的是三维空间中闭合曲面能否连续变形为球面，其数学证明早在二十多年前已由佩雷尔曼给出并获菲尔兹奖认可。但人类写下的证明由自然语言与专业符号构成，依赖审稿人的经验判断，任何细微疏漏都可能潜伏多年。形式化要做的是把整个证明翻译成Lean 4这类证明助手能逐行机器验证的代码，每一步推理都由计算机严格核对，不给含糊其辞留任何空间。
难就难在这里。人类证明的一句显然可得，展开成形式化代码可能是数千行严格推导；佩雷尔曼的原始证明使用了不少非常规技巧，理解门槛本就极高，翻译成机器语言更是难上加难。这也是为什么此前的形式化里程碑多集中于费马大定理等经典结果，而庞加莱猜想的技术复杂度让多数团队望而却步。
这组数据里最值得琢磨的是效率的量级变化。传统形式化是人力密集型工作，一个顶尖团队形式化一条中等难度定理往往以年计。北大团队的路径是把大语言模型嵌入工作流：模型负责把数学证明批量翻译成Lean代码草稿，人类研究者负责审校关键步骤、修补验证失败的地方，编译器的报错信息再反过来指导模型修正，人机在验证闭环里高速迭代。
3万美元的成本几乎全部是调用商用模型的 API 费用，没有专用算力集群，没有自研基座模型。这说明形式化领域的突破已经不取决于谁的模型最强，而取决于谁能把现有模型编排得更高效：提示词设计、错误反馈机制、证明拆解粒度，这些工程细节共同决定了一次验证通过率，也决定了项目的总账单。对资源有限的学术团队来说，这个示范意义直接而现实。
形式化成果的可信度来自验证机制本身。Lean的内核会逐条核对每一步推理是否符合公理体系，任何无法核对的步骤都会被编译器拒绝，所谓双检验是指证明通过了两套独立的核对流程，确保没有依赖验证器自身的漏洞。更进一步，北大团队与美国团队的成果相互独立，两套代码由不同的人机流程产出，却在同一个数学结论上汇合，这种独立互证类似于实验科学里的重复实验，交叉验证了成果的可靠性。
把两份证明的规模放在一起看也有意思：320万行与470万行，差距超过四成。同一目标的代码规模差异，反映的是形式化风格与拆解策略的不同，这也正是形式化作为一项工程活动的自由度所在。未来围绕这些代码库的维护、复用与教学改造，会是一个持续多年的公共工程。
必须划清一条边界：形式化验证的是已有证明，不是提出新证明。庞加莱猜想的数学荣誉仍属于佩雷尔曼，AI在这件事里扮演的是史上最严格的审稿人，而非发现者。但这个角色的价值并不因此打折。数学共同体的一个长期痛点是审稿资源稀缺，复杂证明的审查动辄数年且难保周全，机器验证把正确性判断从专家共识变成机械执行，整个学科的信任基础设施被抬升了一个层级。
往前看，这条路径的终点指向AI辅助发现新数学：当形式化环境足够成熟，模型可以在机器可验证的空间里探索证明路径，正确的猜想自动留下，错误的方向即时淘汰。从验证到猜想再到发现，梯度已经清晰。对国内科研体系而言，这次成果还证明了一件事，在AI for Science的竞赛里，善用公开模型加一流领域知识，同样能打出世界级成果，不必等一块自研芯片或一个大参数基座就位才动手。数学是AI最先攻下的科学堡垒，现在这座堡垒的城墙又矮了一截。
这次成果的另一个注脚是路径选择。团队没有等待自研基座模型或专用算力就位，而是直接调用公开的商用大模型，把精力放在工作流编排与数学知识的工程化上。3万美元的预算规模，让全球任何一个数学系、任何一个研究小组都能负担类似的尝试，这种轻资产的参与方式，把AI数学研究的门槛从巨头专属拉回到了学术社区，让最懂定理的人直接上手编排工具，而不是等待技术条件成熟。
对国内科研体系而言，这个样本的价值在于方法论：在AI for Science的各个分支上，领域知识与大模型编排能力的结合，往往比单纯堆算力更能率先出成果。Lean社区多年积累的开源证明库、开放模型的能力外溢、加上一流数学家的判断力，三者的组合足以支撑世界级的工作。数学是AI最先攻克的科学堡垒之一，而这次攻下城墙一角的方式，恰恰是最便宜也最可复制的那种，这或许比成果本身更值得写进经验册。至少对科研管理者来说，这是一笔投入产出算得清、风险可控的账，值得在更多学科复制。