Mistral AI 刚开源了 Leanstral 1.5，这是个专门跑 Lean4 形式化数学证明的模型。架构有点意思，总参数量 119B，但推理时只激活 6B 参数。协议是 Apache-2.0，完全开源。
在 miniF2F 形式化基准上，验证集和测试集完成率都到了 100%。数学竞赛 PutnamBench 解决了 587 道题（共 672 道，成功率 87.3%）。抽象代数 FATE 系列里，硕士难度的 FATE-H 准确率达到 87%，博士难度的 FATE-X 做到 34%。这几个分数都是目前该领域的历史最佳。
成本这块差距非常大。拿 PutnamBench 的单题平均成本来看，Leanstral 1.5 只要 $4，而字节跳动的 Seed-Prover 1.5 单题成本超过 $300，是前者的 75 倍以上。Aleph Prover 的成本在 $54 – $68 之间。
工程落地场景里，这模型在 57 个代码仓库里成功抓出了 47 个违反属性的漏洞，其中 11 个指向真实缺陷，还有 5 个是 GitHub 以前没报过的潜在问题。
参数规模确实不是决定 AI 推理能力的唯一瓶颈。用 Leanstral 1.5 跑通这个流程，证明只要把激活参数压到 6B，就能发挥 119B 模型的能力。这种高效激活的架构，比单纯堆参数规模更能解决算力成本过高的问题，也让形式化数学证明在工业界落地变得经济上可行。
