Mistral AI open-sources Leanstral 1.5, reducing proof cost to $4 per problem

According to Beating Monitor, Mistral AI has open-sourced Leanstral 1.5, a model designed for formal proofs in Lean 4. The model has a total of 119 billion parameters, with approximately 6.5 billion activated parameters, and is released under the Apache-2.0 license with free API access. Official evaluations show that Leanstral 1.5 solved 587 out of 672 problems on PutnamBench, achieving 87% and 34% accuracy on the abstract algebra benchmarks FATE-H and FATE-X, respectively—setting new state-of-the-art results for models in this category. The average cost to solve a problem on PutnamBench is approximately $4, significantly lower than the tens to hundreds of dollars required by previous systems. As the token budget per problem increases, its success rate continues to rise; in a complex proof involving AVL trees, the model completed the proof after over 2.7 million tokens of reasoning and 22 rounds of context compression. Beyond mathematical proofs, Leanstral 1.5 has also been applied to code verification, where the team identified 11 real bugs across 57 open-source Rust repositories, five of which had not been previously reported.