Mistral AI, a European artificial intelligence company, has recently officially launched Leanstral 1.5, a specialized model for formal mathematical proof. This model is specifically designed for the Lean4 programming language, with a total parameter scale of 119B, but only 6B parameters are activated during actual reasoning, achieving remarkable proof capabilities with extremely low computational costs, and it is completely open-sourced under the Apache-2.0 license.

image.png

On core benchmark tests, Leanstral 1.5 delivered an almost perfect performance. It achieved a 100% completion rate on both the validation set and test set of the miniF2F formal mathematics benchmark, and successfully solved 587 out of 672 Lean4 problems in the PutnamBench math competition. For the FATE series benchmarks in the field of abstract algebra, the FATE-H at the master's level reached 87%, and the FATE-X at the doctoral level reached 34%, both of which are the best results to date.

The cost of solving problems is just one percent of the competitors'

More impressive is the cost advantage of Leanstral 1.5. On the PutnamBench dataset, the model requires only $4 per problem on average, while ByteDance's Seed-Prover 1.5 requires over $300, and Aleph Prover also needs between $54 and $68. This means that with the same workload, the reasoning cost of Leanstral 1.5 is about one percent of the strongest competitor, clearing economic barriers for the large-scale application of formal mathematical proofs.

In practical engineering scenarios, Leanstral 1.5 also demonstrated its solid practical value. The model identified 47 violating attributes in the 57 tested code repositories, including 11 pointing to real code defects, and 5 of them were completely new issues never reported on GitHub before. From pure mathematical competitions to real software engineering verification, this model is proving a fact: parameter size is not the only barrier to capability, efficient activation is the key to bringing AI reasoning capabilities into practical use.