Mistral AI·· 2026-07-02精选AI 评分60
Mistral 发布 Leanstral 1.5：Apache-2.0 免费模型，开放权重与免费 API
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%。
推荐理由
免费 Apache-2.0 模型开放权重和 API，做 Lean 4 形式化验证的可以直接换用，成本约每道题 $4。
来源：Mistral AI · mistral.ai