你要怎么证明一段代码没有安全漏洞？把这个问题抛给传统测试团队时，答案通常是“多写几个单元测试”。但单元测试只能证明“存在某条路径没出错”，无法证明“所有路径都不会出错”。在航空航天、自动驾驶、金融合约这些出一次错就可能致命的领域，形式化验证，用数学严格证明代码的正确性，才是终极答案。
而这条路，过去只有极少数人能走。
2026年6月30日，法国AI公司Mistral AI发布Leanstral 1.5，一款面向Lean 4证明助手的开源形式化证明模型。119B总参数、仅6B活跃参数、Apache-2.0许可证、免费API。这组数字组合在一起，传递了一个清晰信号：形式化证明不再是数学天才和顶级实验室的专属工具，它正在变成每个开发者都能调用的基础设施。
一组数据，重写赛道格局
Leanstral 1.5交出的成绩单，用一组数字就能说清楚。
在miniF2F基准测试上，Leanstral 1.5达到了“饱和”，所有题目全部通过，完成了这个形式化证明领域最权威基准之一的终极挑战。这意味着什么？Goedel-Prover-V2-32B，2025年8月发布时被称为“最强开源定理证明器”，在pass@32设置下得分为88.1%（自校正模式90.4%）。DeepSeek-Prover-V2-671B，一个671B参数的庞然大物，得分82.4%。Leanstral 1.5用6B活跃参数做到了100%，比第二名高出近10个百分点，参数规模仅为对手的不到百分之一。
在Putnam数学竞赛基准上，Leanstral 1.5证明了587道题（共672道），正确率87.35%。Putnam竞赛是美国和加拿大最顶尖的本科数学竞赛，题目以深度和难度著称。对比之下，Goedel-Prover-V2-32B在pass@192下解决了86道，DeepSeek-Prover-V2-671B在更宽松的pass@1024下也仅解决47道。Leanstral 1.5的成绩是次优方案的近7倍。
在FATE-H基准上，一个测试研究生级别抽象代数能力的基准，涉及群论、环论、模论，Leanstral 1.5取得87%的SOTA成绩。在更高难度的FATE-X（博士级别）上，也达到了34%。
但真正让这些数字变得有说服力的，不是分数本身，而是达成分数的方式。
把推理时间变成解题力
Mistral在Leanstral 1.5的公告中披露了一张关键图表：随着单次尝试的token预算从2.5万增加到400万，PutnamBench的解题数从44题一路爬升到587题，整整13倍的增长，曲线平滑得近乎理想。
这听起来简单，实际做起来极难。
大多数大模型在推理过程中遇到困难时，要么给出错误答案并“自信地”结束，要么陷入无限重复的循环。Leanstral 1.5展现了一种截然不同的行为模式：它不放弃。当一条证明路径走不通时，它会编辑文件、回退、换一条路、再试。在一个AVL树平衡证明的案例中，Leanstral 1.5连续推理了超过270万个token，跨越22次“压缩”（compactions），最终输出了一个完整的、经过验证的O(log n)复杂度证明。
这种“test-time scaling”能力，即推理时投入越多计算资源模型表现越好，是形式化证明领域最稀缺的属性。它把AI数学证明从一个“碰运气”的问题变成了一个投入产出比可预期的问题。Mistral表示，这是他们见过的形式化推理模型中最强的test-time scaling表现。
不止于数学竞赛，从理论到实战
Leanstral 1.5的野心不止于解决数学竞赛题。Mistral构建了一套自动化的bug发现流水线：Aeneas工具将Rust代码翻译为Lean，Leanstral 1.5从中推断代码的使用意图并生成正确性属性，然后尝试证明这些属性。如果四次尝试全部失败，它会反过来尝试证明反例也成立。如果反例也被证否，就确认了bug的存在。
在57个开源仓库的测试中，这套流水线标记了47个违反的属性，其中11个指向了真正的bug，5个是此前从未在GitHub上报告过的未知漏洞。
其中一个典型案例：在datrs/varinteger库的zigzag解码函数中，当输入值为Std.U64.MAX时，表达式(value + 1)会发生整数溢出。调试模式下程序崩溃，发布模式下数据静默损坏。这是传统的测试和模糊测试几乎不可能捕捉到的边缘情况，但Leanstral 1.5的流水线自动抓住了它。
这个案例揭示了形式化验证的真实价值：它知道你的代码在什么时候会“静默地出错”。这是所有测试方法都无法保证的。
为什么是现在
Leanstral 1.5的发布不是一个孤立事件。它发生在形式化证明领域正在经历一场基础设施革命的历史窗口期。
2026年5月，DeepMind发布了AlphaProof Nexus，声称自主解决了9个Erdős开放问题。同月，OpenAI的ChatGPT 5.5被披露内部用于发现了一个关于off-diagonal Ramsey数的Lean验证证明。《经济学人》专题报道了以Lean为核心的AI数学创业公司。Terence Tao，当代最著名的数学家之一，已经在自己的YouTube频道上定期直播用Lean做AI辅助证明。
Lean 4这个证明助手本身，正在从学术界的小众工具变成AI巨头们比拼推理能力的竞技场。截至2026年6月，它的mathlib库获得了Demailly开放科学奖，最新稳定版4.31.0于6月15日发布。Goedel-Prover、DeepSeek-Prover、AlphaProof、Leanstral。不到两年时间，形式化证明赛道已经挤满了顶级玩家。
但Leanstral 1.5选择的路线和其他人不一样。
它没有走“大模型加巨大的推理预算”的路。AlphaProof Nexus背后的计算成本仍然是谜。它走的是极致的效率。6B活跃参数，128个专家模块每token只激活4个，MoE架构的稀疏性让推理成本降到了其他方案的几十分之一。Apache-2.0许可证意味着任何团队都能下载权重，在自己的硬件上跑、在自己的代码库上配置、嵌入自己的CI/CD流水线。
Leanstral 1.5的哲学是：让所有人都能拥有“证明的丰盈”。Proof Abundance for All。
局限与未解之问
当然，Leanstral 1.5并非完美。
在FATE-X（博士级别抽象代数）上的34%说明，顶级的数学前沿问题仍然是它力所不能及的。57个开源仓库中发现5个此前未报告的bug，这个数量不算巨大。它目前主要擅长处理有明确正确性规格的问题，对于依赖人类直觉的模糊代码逻辑，适用性还有限。
另一个值得关注的点：Mistral并未在公告中提供Leanstral 1.5与上一代Leanstral（2026年3月发布）的直接对比数据。这意味着我们无法量化1.5比1.0进步了多少。部分行业观察者也注意到了这一点。
但瑕不掩瑜。问题的关键不在于Leanstral 1.5是否完美，而在于它是否把形式化验证推进到了可日常使用的临界点。从目前的证据来看，答案很可能是“是的”。
更远的远方
形式化验证正在经历从“手工奢侈品”到“自动化基础设施”的转变。Leanstral 1.5站在这个转变的拐点上，用一组让人无法忽视的数据向行业证明：形式化验证不再是顶会论文里的未来，而是今天就能用的工具。
当AI不仅能帮你写代码，还能证明你写的代码没有bug时，软件开发的质量下限会被整体抬升。而在航空、医疗、金融、自动驾驶这些每次出错都可能致命的领域，这意味着什么，不言而喻。
如果说2026年AI行业的主旋律是Agent化，那么Leanstral 1.5给出了一个更加深层的叙事：Agent要能做，还要能证明自己做得对。这或许才是可信AI的真正起点。
证明的丰盈时代，刚刚开始。
快报