法国AI公司Mistral AI发布了开源模型Leanstral，专为Lean 4工作流程设计，并以代码代理形式提供。除了生成代码外，Leanstral还能处理形式化证明相关任务。官方同时以Apache 2.0许可证发布模型权重，集成至Mistral Vibe代理框架，并提供labs-leanstral-2603实验性API端点，开发者可通过云端或本地环境使用。

Leanstral聚焦于Lean 4工作流程，而非通用型编程助手。Lean 4是一套用于形式化证明的证明辅助工具与编程语言，可用于表达数学定理与软件规范。Mistral表示，Leanstral的训练目标是让模型能够在贴近实际的形式化代码库中工作，而非仅解决单个数学题或简单包装通用大模型。官方强调，该模型支持MCP，并针对常用工具lean-lsp-mcp进行了专门优化。

Mistral已将Leanstral直接整合进Mistral Vibe。根据官方模型页面说明，用户可在Vibe中通过/leanstral指令安装Leanstral代理，也可使用vLLM在本地部署模型。Hugging Face模型页面显示，Leanstral采用稀疏MoE架构，支持工具调用、长上下文处理与多语言能力。

Mistral同步推出了名为FLTEval的新评估基准，作为Leanstral的主要测试依据。官方说明，FLTEval不依赖竞赛数学题，而是以FLT项目拉取请求中的形式化证明补全与新概念定义为测试场景。Mistral公布的数据表明，Leanstral在pass@2时得分为26.3，高于Claude Sonnet 4.6的23.7；在pass@16时得分为31.9，但Claude Opus 4.6仍以39.6领先。

官方在案例中列举了两类应用场景：一类是处理新版Lean引发的兼容性问题，例如协助识别def与abbrev在定义等价上的差异，修正rw tactic无法匹配的情况；另一类是将Rocq中的语义定义转换为Lean，并进一步完成部分程序性质的证明。从目前公开信息看，Mistral此次产品更新主要是将开源代码代理的应用范围，从通用软件开发扩展至形式化验证领域。

Mistral预告后续将发布技术报告，详细说明Leanstral的训练方法，并公开FLTEval基准，以弥补现有评估体系过度侧重竞赛数学题的局限。目前，Leanstral已可通过Hugging Face模型页面和Mistral Vibe相关文档获取与部署。