Mistral AI 发布面向 Lean4 数学形式化证明语言的开源模型 Leanstral 1.5，采用 Apache-2.0 许可，参数总量 119B、激活参数 6B。该模型在 miniF2F 验证集和测试集完成率均为 100%，在 PutnamBench 672 道题中解答 587 道，FATE-H 达成率 87%、FATE-X 达成率 34%。Mistral AI 称，Leanstral 1.5 求解 PutnamBench 单题平均成本约 4 美元，低于 Seed-Prover 1.5 和 Aleph Prover。代码库测试中，该模型识别 47 个违规属性，其中 11 个确认为真实缺陷。
