Mistral 发布 Leanstral 1.5：专注 Lean 4 证明工程的开源模型

Mistral 近日推出 Leanstral 1.5，这是一款面向 Lean 4 证明工程（proof engineering）的开源模型，号称在该方向达到了当前最优水平（SOTA）。模型权重已同步发布至 Hugging Face，供开发者下载与研究。

模型定位

Leanstral 1.5 由 Mistral 发布，名称融合「Lean」与「Mistral」，定位十分明确：专为 Lean 4 这一形式化证明语言提供 AI 能力支持。它属于 Mistral 模型矩阵中面向特定领域（domain-specific）的最新成员，并非通用大模型迭代。

关于 Lean 4 与证明工程

Lean 4 兼具通用函数式编程语言与交互式定理证明助手的双重身份。开发者既可用它编写 CLI 工具与库，也能借助其证明引擎，对代码、协议和算法的关键性质进行机械化验证。近年来，AI 辅助定理证明逐渐成为研究热点，Lean 4 在数学形式化、软件验证、密码协议校验等场景的关注度持续提升。

开源与可用性

Leanstral 1.5 以开源权重形式发布，托管在 Hugging Face 平台上，遵循相应的开源协议（具体许可证尚待官方确认）。研究者和工程团队可直接下载权重进行推理、微调，或在本地及私有环境中部署，无需依赖闭源 API。这延续了 Mistral 在开源生态上的一贯策略。

信息局限

目前公开信息仍然有限——包括模型参数量、训练数据构成、在 miniF2F、ProofNet 等主流数学证明基准上的具体表现，以及相对此前版本（若存在 Leanstral 1.0）的能力提升幅度，均尚未披露。对于从事形式化验证、定理证明或 AI for Math 研究的小众群体而言，Leanstral 1.5 提供了新的基线选项；但要评估其实际价值，仍需等待更完整的技术报告与社区评测。