Mistral's open-source Leanstral 1.5 aces formal math benchmarks and catches real bugs in code

Mistral AI released Leanstral 1.5, an open-source model for formal verification in Lean 4, achieving 100% on miniF2F and 87% on FATE-H. It also solved 587 of 672 problems on PutnamBench and detected five unknown bugs across 57 repositories, including a Rust overflow issue. Available via Hugging Face and a free API, the model combines mid-training, supervised fine-tuning, and reinforcement learning.