Mistral AI·· 2026-07-02精选AI 评分66
Mistral 发布 Leanstral 1.5，形式化验证性能升级并开源
Leanstral 1.5: Proof Abundance for All
AI 导读
Mistral 发布 Leanstral 1.5，一个 Apache-2.0 许可、119B 总参数 6B 激活参数的模型，在形式化验证上大幅升级，miniF2F 达到 100%，PutnamBench 解出 587/672 题，FATE-H 达 87%、FATE-X 达 34%。
推荐理由
官方给出 Leanstral 1.5 在形式化验证基准上的成绩与开源入口，读者可据此判断其在 Lean 4 证明工程中的可用性。
来源：Mistral AI · mistral.ai