Mistral AI 刚刚把 Leanstral 1.5 开源了，119B 总参数（仅 6B 激活参数）的 MoE 模型，Apache-2.0 完全开源，专为 Lean 4 形式化证明和自动定理证明优化。

完全饱和 miniF2F（100%）；PutnamBench 解决 587/672 个问题；FATE-H 达到 87% SOTA，FATE-X 达到 34% SOTA。

在 PutnamBench 上以约 $4/问题 的预算达到领先表现，比某些竞品便宜 10 倍 左右，同时改善 Pareto 前沿。

在 PutnamBench Pass测试中，token 预算从 25k 提升到 4M 时，性能持续平稳上升（从 44 个到 587 个问题）。支持长达数百万 token 的多轮推理和上下文压缩。

虽主训数学，但在真实开源仓库中自动发现 5 个此前未知的 bug（在 57 个仓库中检测出 11 个真实 bug）。通过 Aeneas 将 Rust 代码转 Lean 并生成正确性属性。

采用 mid-training + SFT + RL（CISPO），支持多轮证明环境和代码代理环境，可在 Lean 4 中编辑文件、运行命令、利用语言服务器实时反馈。

权重代码已开源，同时 Mistral 官方也提供免费的 API 接口供全球开发者直接调用体验，感兴趣的可以直接去调用尝鲜。