Mistral AI 正式推出 Leanstral 1.5，一个专为 Lean 4 证明助手打造的开源代码智能体模型，参数规模达 119B，采用 Apache 2.0 许可，已在 Hugging Face 上架。该模型基于 Mistral Small 4 家族架构，每 token 仅激活 6.5B 参数，兼顾性能与成本效率。
Leanstral 1.5 的核心定位是成为 Lean 4 环境中的 AI 编程与证明伙伴。Lean 4 本身是一种强大的证明助手，能够表达极其复杂的数学结构——例如 完美空间（perfectoid spaces）——以及形式化软件规范，如 Rust 代码片段的属性验证。这意味着 Leanstral 1.5 的应用场景远不止通用代码生成，而是直接切入数学定理证明、形式化验证等高门槛、高价值的科研与工业领域。
在技术架构上，该模型采用了 混合专家（MoE） 设计，共包含 128 个专家，每个 token 激活其中 4 个。这种稀疏激活机制使得模型在保持 119B 总参数规模的同时，推理计算量仅相当于一个约 6.5B 激活参数的稠密模型。模型支持 文本与图像多模态输入，上下文窗口达 256k token，官方建议在实际使用中控制在 20 万 token 以内以保证稳定性。
部署方面，Mistral 提供了两条路径。用户可以直接通过 Mistral API 调用，无需订阅 Pro 计划，只需在账户设置中开启“Labs models”选项并生成 API 密钥，再通过 Mistral Vibe CLI 工具即可启动 Leanstral 智能体。对于偏好本地部署的用户，模型同样兼容 vLLM 推理框架，官方给出了详细的服务器启动参数与客户端调用示例，推荐使用张量并行（tensor parallelism）为 4 的配置，并启用 Flash Attention MLA 后端以优化长上下文推理效率。
Leanstral 1.5 的发布延续了 Mistral 在开源模型领域的激进策略。与闭源的通用大模型不同，Leanstral 1.5 聚焦于一个极为细分的专业赛道——形式化数学与软件验证。这一领域长期以来由人类专家主导，自动化程度有限。AI 代码智能体的介入，有望大幅降低 Lean 4 的使用门槛，加速数学研究中的证明编写与检查流程，同时为安全关键软件（如操作系统内核、加密协议）提供更高效的形式化验证手段。
从产业视角看，Leanstral 1.5 的出现可能对算力需求结构产生微妙影响。数学证明与形式化验证任务通常需要长时间的链式推理，对模型的长上下文处理能力和推理连贯性要求极高，这与通用对话或代码补全的负载特征不同。若此类专用模型在学术界和工业界获得采用，可能会催生对高吞吐、长上下文推理优化的算力需求，间接影响 AI 基础设施层 的硬件与软件栈设计。
此外，Leanstral 1.5 基于 Mistral Small 4 家族构建，表明 Mistral 正在将其基础模型能力向多个垂直方向延伸。此前 Mistral 已在通用对话、代码生成等领域布局，此次切入数学证明，进一步丰富了其开源模型矩阵。在开源社区中，一个专攻 Lean 4 的强模型可能吸引更多研究者参与形式化数学与验证工具的生态建设，形成正向循环。
Mistral 同时提醒，该模型是对此前 Leanstral 版本的更新迭代，建议用户通过 lean-lsp-mcp 工具与 Leanstral 交互，以获得更流畅的开发体验。对于复杂任务，官方推荐将推理强度（reasoning effort）设为“high”，并允许模型进行长时间、多步骤的问题求解——Leanstral 被设计为能够处理需要数小时持续工作的长程任务。