Mistral has open-sourced Leanstral 1.5 under the Apache 2.0 licence, bringing advanced AI-powered theorem proving and automated code verification to developers and enterprises with self-hosting support.
Mistral AI has released Leanstral 1.5 as an open-source AI model under the Apache 2.0 licence, expanding access to advanced formal verification for mathematical proofs and software correctness. The permissive licence enables commercial use, modification and self-hosting, making the model suitable for organisations with strict compliance and data governance requirements.
Designed to work with the Lean 4 interactive theorem prover, Leanstral 1.5 targets both academic mathematics and practical software verification. It is available through a free API endpoint and via Hugging Face for self-hosting. The model uses a Mixture-of-Experts architecture with 119 billion total parameters, of which 6 billion are active during inference.
According to Mistral, Leanstral achieved 100% on both the validation and test sets of the miniF2F benchmark and solved 587 of 672 problems on PutnamBench, which evaluates logical reasoning and long proof chains. The company also said the model required only one-seventh of the computation that Opus 4.6 would have consumed for the same PutnamBench task. Leanstral also solved 87 graduate-level abstract algebra tasks on FATE-H and 34 doctoral-level tasks on FATE-X.
Mistral also demonstrated an automated Rust verification pipeline using Aeneas, which translates Rust code into Lean before Leanstral proves or disproves correctness properties. Tested across 57 open-source Rust repositories, the pipeline detected 47 violated properties, confirmed 11 genuine bugs, including five previously unreported on GitHub. The release follows Mistral’s recent launch of Mistral OCR 4.
