Mistral发布Leanstral：Lean4首个开源代码Agent，生成代码同时输出形式化证明

据 1M AI News 监测，Mistral AI 今日发布 Leanstral，首个专为形式化验证工具 Lean 4 设计的开源代码 Agent。AI 代码生成的核心瓶颈是人工审查，Leanstral 让 AI 生成代码的同时输出可被 Lean 4 自动校验的形式化证明，绕开这一环节。模型采用稀疏 MoE 架构，120B 总参数、6B 激活参数，Apache 2.0 开源，针对 lean-lsp-mcp 做了专项训练优化。可在 Mistral Vibe 中零配置启动（命令 /leanstall`），或通过免费 API 端点 `labs-leanstral-2603 调用，支持下载权重自部署。

Mistral 同步发布了新评估基准 FLTEval，以 Lean 4 社区的费马大定理形式化项目为测试场。成本对比：Leanstral pass@2 以 $36 得分 26.3，超过成本 $549 的 Claude Sonnet 4.6（23.7 分）；pass@16 以 $290 得分 31.9，领先 Sonnet 8 分，而 Claude Opus 4.6 需 $1,650 才达到 39.6 分。开源模型中，Qwen3.5-397B-A17B 需运行 4 次才到 25.4 分，仍低于 Leanstral pass@2。