Mistral Releases Leanstral 1.5, an Open Model That Solved 587 of 672 Putnam Math Problems

Mistral AI has released Leanstral 1.5, an open-source 119B mixture-of-experts model (with ~6B active parameters) specialized in writing and verifying formal proofs in Lean 4. It solved 587 of 672 Putnam math competition problems and achieved 100% on the miniF2F benchmark. Beyond math contests, the model operates as a code agent that can scan real codebases — it already found five previously unknown bugs across 57 open-source repositories. It uses a compiler-validated feedback loop rather than model-on-model review, offering a more trustworthy correctness guarantee. Performance scales with token budget, from 44 problems at 50K tokens to 587 at 4M tokens. Released under Apache 2.0, it's available via Mistral's Labs tier, Hugging Face, and local deployment with vLLM.