写形式化证明，像是在一位极严格的检查员面前写代码：模型可以反复尝试，但每一步最终都要由 Lean 4 的可信内核核验。新进入模型热榜的 Leanstral 1.5，正是为这类工作设计的开源代码 Agent——它会生成证明代码、读取工具报错，再修改方案。
据 Mistral 模型页，Leanstral 1.5 属于稀疏 MoE 模型：总计 119B 参数，设有 128 个“专家”模块，但处理每个词时只启用其中 4 个，约激活 6.5B 参数。换句话说，它像一支规模很大的专家团队，每次只叫最相关的几位上场，因此单步计算量更接近 6.5B，而不是 119B。不过，全部权重仍需存放，不能把它当成普通 6.5B 模型看待。
模型还支持文本与图像输入，标称上下文长度为 256k tokens，官方建议实际控制在 200k 以内，并提供基于 vLLM 的本地部署方式。值得观察的是，它把大型模型的容量与较低的单步激活量放进了可本地部署的 Lean 证明场景；但材料没有给出基准测试或本地硬件需求，实际效果与部署门槛仍待验证。