Mistral AI 发布了 Leanstral，这是首个专为形式化验证工具 Lean 4 设计的开源代码 Agent。
核心突破
它能在生成代码的同时，输出可由 Lean 4 自动校验的形式化证明，旨在绕过人工审查这一核心瓶颈。
技术要点
- 架构：采用稀疏 MoE 架构，总计 120B 参数，激活参数为 6B。
- 许可：Apache 2.0 开源。
- 优化：针对
lean-lsp-mcp进行了专项训练优化。
使用方式
- 在 Mistral Vibe 中可通过命令
/leanstall零配置启动。 - 可通过免费 API 端点
labs-leanstral-2603调用。 - 支持下载模型权重自行部署。
性能与成本
Mistral 同步发布了新评估基准 FLTEval（以费马大定理形式化项目为测试场）。
- Leanstral pass@2：以 36 美元成本获得 26.3 分，优于成本 549 美元的 Claude Sonnet 4.6（23.7分）。
- Leanstral pass@16：以 290 美元成本获得 31.9 分，领先 Claude Sonnet 8 分。
- 对比开源模型，Qwen3.5-397B-A17B 需运行 4 次才达到 25.4 分，仍低于 Leanstral pass@2 的表现。
