Mistral 发布 Leanstral 1.5：开源形式化验证模型

Mistral 于 2026 年 7 月 2 日发布 Leanstral 1.5，采用 Apache 2.0 许可。

该模型为 119B 参数的 MoE 架构，专为 Lean 4 证明助手构建。

据称在 PutnamBench 上解出 587/672 题，并在 57 个开源仓库中发现 5 个此前未知的 bug。

模型提供免费 API 端点，权重可在 Hugging Face 下载。