**"[Theorem Proving Gets Competitive on Costs: Mistral Open-Sources Leanstral 1.5, Costing Around $4 Per Problem]** According to monitoring by 动察 Beating, Mistral AI has open-sourced Leanstral 1.5, a model designed for formal theorem proving in Lean 4. The model has a total of 119 billion parameters, with approximately 6.5 billion active parameters. It is released under the Apache-2.0 license and offers free API access. Official evaluations show that Leanstral 1.5 solved 587 out of 672 problems on PutnamBench. It achieved 87% and 34% accuracy on the abstract algebra benchmarks FATE-H and FATE-X, respectively, setting a new performance record for similar models. The average cost per problem solved on PutnamBench is approximately $4, significantly lower than the tens to hundreds of dollars required by some previous systems. As the token budget per problem increases, the number of problems solved by the model continues to grow. For example, in the complexity proof of AVL trees, the model completed the proof after reasoning through over 2.7 million tokens and performing 22 rounds of context compression. In addition to mathematical theorem proving, Leanstral 1.5 has also been applied to code verification. The team discovered 11 real bugs across 57 open-source Rust repositories, 5 of which had not been previously reported. [Original Link]"**