Theorem Proving Also Starting to Roll Its Own: Mistral Open Sources Leanstral 1.5, Priced at around $4 Per Theorem

According to Perceive Beating monitoring, Mistral AI has released Leanstral 1.5, a model for Lean 4 formal proofs. The total model parameters are 119 billion, with around 6.5 billion activation parameters. It is released under the Apache-2.0 license and provides free API access.

Official benchmarks show that Leanstral 1.5 solved 587 out of 672 problems in PutnamBench. It achieved 87% and 34% on the abstract algebra benchmarks FATE-H and FATE-X, respectively, setting a new record among similar models.

The average cost of solving problems in PutnamBench with Leanstral 1.5 is approximately $4, lower than the tens to hundreds of dollars cost of some previous systems. As the budget per problem token increases, the number of problems solved continues to rise. In an AVL tree complexity proof, the model underwent over 2.7 million token inferences and 22 instances of context compression to eventually complete the proof.

In addition to mathematical proofs, Leanstral 1.5 has also been used for code verification. The team discovered 11 real bugs in 57 open-source Rust repositories, 5 of which were previously unreported.