近日，Mistral AI 正式发布了专为数学形式化证明语言 Lean4 设计的开源模型——Leanstral 1.5。该模型采用 Apache-2.0 许可协议，总参数 119B，但推理时仅激活 6B 参数，在保持高性能的同时大幅优化成本。 在权威的 miniF2F 基准测试中，Leanstral 1.5 的验证集和测试集均达到 100% 完成率。面对 PutnamBench 数学竞赛题库，它从 672 道 Lean4 问题中成功解答 587 道。在抽象代数领域的 FATE 系列测试中，硕士级 FATE-H 达成率 87%，博士级 FATE-X 达成率 34%，均刷新纪录。 成本优势突出：平均每道 PutnamBench 题目求解成本仅 4 美元，而对比模型 Seed-Prover 1.5 超过 300 美元，Aleph Prover 则在 54–68 美元之间。此外，在对 57 个代码库的实测中，模型识别出 47 个违规属性，其中 11 个为真实缺陷，5 个漏洞此前从未在 GitHub 上被报告，展现了其在代码验证与安全审查中的潜力。