Mistral 发布 Leanstral 开源形式化代码智能体

Mistral 发布 Leanstral，首个专为 Lean 4 设计的开源代码智能体，采用 6B 激活参数架构。在 FLT 项目验证基准上，其 pass@2 得分超越 Claude Sonnet 4.6，且运行成本仅为后者的约 1/15。模型以 Apache 2.0 协议开源，支持 Mistral Vibe 集成与 MCP 工具调用。