Mistral AI 正式开源了一款专注于形式化验证的大模型 Leanstral 1.5，该模型针对 Lean 4 自动定理证明任务进行了专门优化。其采用 1190 亿参数的混合专家（MoE）架构，每个 token 仅激活 65 亿参数，不仅支持 256k 的超长上下文窗口，还具备图文输入能力。在 miniF2F、PutnamBench 等主流数学证明基准测试中，Leanstral 1.5 取得了当前最优（SOTA）的性能表现。目前，该模型已在 HuggingFace 平台开源，用户可实现本地部署或在线体验。