Mistral 发布 Leanstral 1.5：6B 激活参数的开源形式化证明模型

Mistral 发布 Apache-2.0 开源的 Leanstral 1.5，总参数 119B、激活 6B，专注 Lean 4 形式化证明。模型饱和 miniF2F（验证与测试集均 100%），在 PutnamBench 解出 587/672 题，FATE-H 87%、FATE-X 34% 达到 SOTA，单题成本约 $4。