en.Wedoany.com Reported - European artificial intelligence company Mistral AI announced on the 2nd of this month local time the launch of the Leanstral 1.5 model, designed for the Lean 4 formal mathematical proof programming language. The model has a total of 119B parameters, with 6B parameters activated, and is open-sourced under the Apache-2.0 license.

Mistral AI stated that the Leanstral 1.5 model achieved a 100% completion rate on both the validation and test sets of the miniF2F formal mathematics benchmark; it solved 587 out of 672 Lean 4 problems in the PutnamBench mathematical competition problem set; for the FATE series of abstract algebra benchmarks, it achieved an 87% success rate on the master-level FATE-H and a 34% success rate on the doctoral-level FATE-X, both representing the best performance. These tests indicate that the model's mathematical capabilities have reached a usable level.

Mistral AI emphasized the cost advantage of the new model: for problems in the PutnamBench dataset, the average solving cost of Leanstral 1.5 is only $4, while Seed-Prover 1.5 requires over $300, and Aleph Prover also requires $54 to $68.

In real-world application scenarios, Leanstral 1.5 flagged 47 violation attributes across 57 tested codebases, of which 11 pointed to actual defects, including 5 issues not previously reported on GitHub.