Leanstral 1.5: Mistral's AI model for formal proofs is open source

Mistral AI has released Leanstral 1.5, a specialized AI model for formal verification and mathematical proofs, the company announced. Licensed under Apache 2.0, the model works with the interactive theorem prover Lean 4 and aims to cover both academic mathematics and practical code verification. The architecture comprises 119 billion parameters in total, of which only 6 billion are active, according to a company blog post. The model is available as a free API endpoint and via Hugging Face for self-hosting. On the miniF2F benchmark, Leanstral 1.5 achieves 100 percent on the validation and test sets, according to Mistral. On the PutnamBench, the model solves 587 out of 672 problems from the Putnam Mathematical Competition. Leanstral's computation reportedly cost only a seventh of what Opus 4.6 would have consumed for the same task, according to Mistral. On the FATE-H and FATE-X benchmarks for abstract algebra at graduate and doctoral levels, Leanstral solves 87 and 34 tasks. Mistral also demonstrates a pipeline for automatic bug detection in Rust projects using a tool called Aeneas, which translates Rust code to Lean. In a test with 57 open-source repositories, the pipeline identified 47 violated properties, 11 of which turned out to be genuine bugs, five of which had not been reported on GitHub previously. The Apache 2.0 license allows for self-hosting, which the company says is relevant for companies with high compliance requirements.