Mistral AI Releases Leanstral 1.5, an Open-Weight Lean 4 Model Setting New Marks on Math-Proof Benchmarks

Mistral AI has released Leanstral 1.5, an Apache-2.0 open-weight model built for formal theorem proving in Lean 4 that solves 587 of 672 problems on PutnamBench while claiming roughly a tenfold cost advantage over leading competitors. The model, detailed in a company blog post published around July 2, 2026, positions itself as one of the strongest openly available systems for automated mathematical proof engineering. Mistral's announcement frames the launch under the banner "Proof Abundance for All."