Recently, Mistral AI officially released an open-source model called Leanstral1.5, specifically designed for the mathematical formal proof language Lean4. The model is licensed under the Apache-2.0 license, with a total of 119B parameters and 6B activated parameters, significantly reducing costs while maintaining high performance.

As an intelligent tool focused on mathematical reasoning, Leanstral1.5 has shown remarkable performance. In the authoritative miniF2F formal mathematics benchmark test, the model achieved a 100% completion rate on both the validation set and the test set. Facing the highly challenging PutnamBench math competition question bank, it successfully solved 587 out of 672 Lean4 problems. Additionally, in the FATE series benchmark tests in the field of abstract algebra, it also demonstrated dominance: achieving an 87% success rate in the master-level FATE-H test, and a 34% success rate in the doctoral-level FATE-X test, setting a new record for this type of model.

image.png

The cost advantage is another core highlight of this model release. Mistral AI emphasized that compared to other solutions on the market, Leanstral1.5 greatly reduces the cost of scientific trial and error. For example, using Leanstral1.5 to solve questions in PutnamBench has an average cost of only $4, while the cost of the comparative model Seed-Prover1.5 exceeds $300, and Aleph Prover's cost ranges between $54 and $68. This significant cost reduction is expected to bring high-precision mathematical proof assistance technology out of the laboratory and serve a broader research community.

In practical code development scenarios, Leanstral1.5 also demonstrated strong "bug-finding" capabilities. In testing 57 code repositories, the model successfully identified 47 violations, among which 11 were verified as real defects. Notably, five of these vulnerabilities had never been reported on GitHub before, proving the great potential of AI in assisting program verification and security reviews.

With the open source of Leanstral1.5, the fields of mathematics and computer science are welcoming a more accessible and efficient proof-assisting tool. By reducing computing power and economic costs, this model is expected to accelerate the popularization of formal mathematical proofs and help researchers free themselves from tedious calculations and verifications, focusing on breakthroughs in core scientific issues.