Leanstral 1.5：Lean 4 形式化证明模型的试用清单
Mistral 面向 Lean 4 形式化证明与代码验证的开放模型，可通过权重或免费 API 试用。
Leanstral 1.5 mistral open-weight-models reasoning-models coding-agent Mistral 面向 Lean 4 形式化证明与代码验证的开放模型，可通过权重或免费 API 试用。
1. 模型定位
Leanstral 1.5 是 Mistral 针对 Lean 4 形式化证明工程和自动形式化推出的模型。官方资料给出 119B 总参数、约 6.5B 激活参数、256k 上下文，并提供 Apache-2.0 权重与 API 入口。[S1][S2] 它的价值在于生成和修订可由 Lean 编译器检查的候选证明，不应被当成无需验证的数学裁判。
2. 适用任务
适合从已有 Lean 仓库里的局部任务开始：补齐一个证明、解释目标状态、迁移小段定理或为代码性质生成候选断言。不要把自然语言需求直接变成关键系统的“已证明安全”结论。用户意图、形式化规格和实现之间仍可能错位，模型通过编译也只说明当前陈述成立。
3. 接入方式
团队可先用 API 验证任务匹配，再决定自托管。官方模型页列出聊天、函数调用、Agents 与结构化输出等接口。[S2] 两条路线都要固定模型、Lean 工具链和依赖；API 与本地结果不能假设一致。
4. 证明环境
建立只含公开或脱敏代码的沙盒，锁定 lakefile、Lean 和依赖版本。命令限制在容器内，禁止访问生产凭据和任意网络。保存目标、修改、编译日志和最终证明。
5. 质量评测
官方发布列出形式化数学和真实仓库评测结果，[S1] 这些数字只能描述其给定设置。内部评测应准备已知可证、不可证、规格错误和依赖缺失四类题目，记录首次通过率、总尝试、token、耗时与人工修订。验收重点是证明可重复编译、没有新增公理和绕过检查的占位符。
6. 安全与审查
对模型生成的 shell 命令、依赖变更和仓库写入设置允许清单。自动证明可能通过修改定理陈述、弱化前提或引入不受信任公理来“解决”任务，因此差异审查必须覆盖规格、imports、编译选项和信任边界。关键库的合并仍需熟悉 Lean 与业务语义的人复核。
7. 同类对比
与通用代码模型相比，Leanstral 1.5 明确围绕 Lean 编译反馈和长程证明工程训练；与传统自动定理证明器相比，它通过语言模型生成策略和代码候选。[S1] 两类工具可以组合：让模型探索，让内核做确定性检查。选择时应比较本地定理集，而非只比较厂商汇总基准。
8. 主要风险
最容易被忽略的是“证明了错误的规格”。模型还可能消耗大量推理预算、反复改写无关文件，或生成难以维护的长证明。API 路线另有代码外传风险，自托管路线则带来显存、依赖与漏洞维护责任。应设置文件范围、时间和 token 上限，并对失败保留清晰退出条件。
9. 上线验收
选取二十个代表性任务进行盲测，至少包含历史缺陷和故意错误规格。成功标准是最终文件在干净环境重复编译，差异仅限授权范围，没有新增未审公理，人工能解释关键不变量，并且成本处于预算内。达标后也只作为证明助手接入代码评审，不自动批准或合并。
10. 来源与更新时间
资料核对日期：2026-08-12。