法国 AI 初创公司 Mistral AI 于 2026 年 3 月 16 日正式发布面向形式证明工具「Lean 4」的 AI 代理「Leanstral」。该模型旨在辅助数学证明与软件规格验证等场景中的“证明工程”（即形式证明的构建与验证工作），并以开源形式对外提供。
面向 Lean 4 的专用证明工程模型
Leanstral 是专为「Lean 4」生态打造的 AI 模型。Lean 4 既是定理证明辅助系统，也是函数式编程语言，广泛用于：
- 数学定理与证明的形式化
- 软件与硬件系统的形式验证
- 程序正确性与安全性的严格证明
在这些高严谨度领域中，研究者与工程师不能只依赖自然语言描述，而必须使用形式化语言来书写证明，并通过工具对其进行机械化验证。Mistral AI 将 Leanstral 定位为针对这类“证明工程”任务深度优化的专用模型。
开源发布，可与 Lean 环境联动的 AI 代理
Leanstral 以 Apache 2.0 许可证开源，其模型权重已在 Hugging Face 上提供，同时也可通过免费的 API 端点进行调用，方便研究者与开发者集成到现有工作流中。
在模型架构上，Leanstral 采用 Mixture of Experts（MoE，专家混合）结构：
- 总参数量约 1190 亿
- 实际参与推理的激活参数约 65 亿
- 支持最长 256k token 的上下文长度
与一般的文本生成模型不同，Leanstral 被设计为可与 Lean 环境深度联动的 AI 代理。它可以与用于解析、操作 Lean 项目的工具集成，从而在以下方面提供支持：
- 辅助构建与补全形式化证明
- 在现有 Lean 项目中导航、定位与修改证明
- 结合 Lean 的检查机制，迭代修正无法通过验证的证明脚本
通过这种方式，Leanstral 不仅生成代码或证明片段，更参与到整个形式证明构建流程中。
缓解人工审核成为瓶颈的问题
在数学证明与形式验证领域，即便使用了自动化工具，最终的正确性保障仍高度依赖人类专家的审核。这一人工审查环节往往耗时巨大，容易成为项目推进的瓶颈。
Leanstral 的设计前提，是让 AI 生成的证明与代码以可被形式化验证的方式呈现，并与 Lean 4 内置的验证机制紧密结合：
- AI 负责生成候选证明、策略或代码
- Lean 4 负责对这些结果进行严格的形式化检查
- 不通过验证的部分可在 AI 与工具链的协作下自动迭代修正
Mistral AI 强调，在安全性要求极高或风险较大的应用场景中，人类专家的最终审阅仍然不可或缺。但借助 Leanstral，可以显著减少重复性、机械化的证明构建与调试工作，从而整体提升“证明工程”的效率。
