Mistral AI released Leanstral 1.5 on July 2, 2026 — Apache 2.0 open-source model for formal verification in Lean 4. Benchmarks: 100% miniF2F saturation; 587/672 PutnamBench; 87% FATE-H and 34% FATE-X (SOTA open-source). Only closed-source Aleph Prover beats it on PutnamBench.
Beyond math, Mistral reports strong code verification. Scanning 57 open-source repos found five previously unknown bugs including an overflow in Rust varinteger library. Available on Hugging Face and free API. Training: mid-training, SFT, and reinforcement learning.
119B total parameters, 6B active (MoE architecture).