Leanstral — Mistral 开源 Lean 4 形式化验证代码智能体

Mistral 发布了 Leanstral，这是首个专为 Lean 4 证明助手设计的开源代码智能体，用于形式化数学和软件验证。Leanstral 采用 Apache 2.0 许可证开源，基于稀疏 6B 活跃参数架构——远小于竞争模型——但在 FLTEval 基准测试中以 pass@2 得分 26.3 超越 Claude Sonnet（23.7），成本仅为后者的十五分之一（36 美元 vs 549 美元）。

Leanstral 通过 lean-lsp-mcp 支持模型上下文协议（MCP）扩展，使 AI 智能体可以在验证工作流中直接调用。模型提供三种使用方式：通过 Mistral Vibe 的 /leanstral 命令零配置集成、免费 API 端点（labs-leanstral-2603），以及可下载的自托管权重。

此次发布还包含 FLTEval 评估套件，超越孤立数学题目，转向真实的形式化代码仓库任务。Leanstral 定位于智能体 AI 与形式化验证的交汇点——智能体不仅编写代码，还能证明代码的正确性。

官方公告：https://mistral.ai/news/leanstral