Mistral 发布 Apache-2.0 开源模型 Leanstral 1.5，6B 激活参数聚焦形式化证明

Mistral 发布 Leanstral 1.5，Apache-2.0 许可，总参数 119B、激活 6B，主打 Lean 4 形式化证明工程。模型饱和 miniF2F，解出 587/672 PutnamBench 问题，在 FATE-H 达 87%、FATE-X 达 34%；经 mid-training、SFT 和 CISPO 强化学习三阶段训练。