Leanstral 发布：面向 Lean 4 的开源代码智能体

Mistral 发布 Leanstral，首个面向 Lean 4 的开源代码智能体，在 FLTEval 基准上以 6B 参数超越多个更大开源模型。它通过 Mistral Vibe 集成、支持 MCP，提供免费 API 和 Apache 2.0 权重；pass@2 得分 26.3 仅需 $36，而 Sonnet 4.6 需 $549。