Theorem proofs are also starting to come down to cost: Mistral open-sourced Leanstral 1.5, costing about $4 per problem.

According to Beating's monitoring, Mistral AI has open-sourced Leanstral 1.5, a model for Lean 4 formal proofs. The model has a total of 119 billion parameters, with approximately 6.5 billion activation parameters. It is licensed under the Apache 2.0 license and offers a free API. Official evaluations show that Leanstral 1.5 solved 587 out of 672 problems on PutnamBench; it achieved 87% and 34% on the abstract algebra benchmarks FATE-H and FATE-X respectively, setting new best performance records for similar models. The average solution cost of Leanstral 1.5 on PutnamBench is approximately $4, lower than the tens to hundreds of dollars cost of some previous systems. As the token budget per problem increases, the number of problems it solves continues to increase; in the AVL tree complexity proof, the model completed the proof after more than 2.7 million token inferences and 22 instances of context compression. In addition to mathematical proofs, Leanstral 1.5 was also used for code verification. The team discovered 11 real bugs in 57 open-source Rust repositories, 5 of which had not been previously reported.