Mistral AI·· 2026-07-02精选AI 评分73
Mistral AI 发布 Leanstral 1.5 形式化验证模型
Leanstral 1.5: Proof Abundance for All
AI 导读
Mistral AI 发布 Leanstral 1.5，这是一个 Apache-2.0 许可的免费模型，119B 总参数、6B active parameters，面向 Lean 4 形式化证明工程。
推荐理由
原文同时给出训练流程、基准和代码验证案例，可用于了解形式化证明模型的工程化进展。
来源：Mistral AI · mistral.ai