Leanstral 1.5: Mistral releases an Apache 2.0 model for Lean 4 proofs
Mistral AI announced the release of Leanstral 1.5 on its official blog (mistral.ai/news/leanstral-1-5/) on 2 July 2026. The model uses a sparse architecture with 119 billion total parameters, around 6 billion of them active, and ships under the Apache 2.0 licence. The weights are on Hugging Face, and Mistral is also offering a free API endpoint called “labs-leanstral-1-5”, scheduled for retirement on 30 September 2026.
Formal verification means proving mathematically that a program behaves exactly as specified. Until now it has stayed confined to critical niches — avionics, rail, cryptography — because writing those proofs by hand takes an enormous amount of human effort.
Mistral says it has "saturated" the miniF2F benchmark, scoring 100% on both the validation and the test set. That means the benchmark can no longer tell models apart, not that Leanstral can prove any theorem you hand it. The model also solves 587 of the 672 problems in PutnamBench and reaches state of the art on FATE‑H (87%) and FATE‑X (34%). Worth stressing: these figures come solely from the official announcement and have not yet been confirmed by independent studies.
Mistral reports — a claim relayed by TestingCatalog — that when plugged into a Rust code verification pipeline across 57 open source repositories, the model flagged 47 violations, 11 of them genuine bugs and 5 never previously reported on GitHub. Among the cases the company cites is an overflow in the sign function used for zigzag decoding in the datrs/varinteger library, which can cause crashes in debug mode and silent corruption in release builds. Here too, there is no public confirmation yet that the maintainers have accepted those bug reports.
Releasing a formal verification model under an open licence is a real step toward wider use of automated verification, a set of techniques traditionally locked inside high-assurance industries. Apache 2.0 means anyone can download the weights and put the numbers to the test themselves — that is how we will find out whether they hold up.
Come Olya ha verificato questa notizia
- Verificato
- I read the official announcement at mistral.ai/news/leanstral-1-5/ and confirmed the date, the architecture (119 billion total / about 6 billion active), the Apache 2.0 licence, the miniF2F, PutnamBench and FATE‑H/FATE‑X figures, the 5 previously unreported bugs found across 57 repositories, and the varinteger case. I then found the same data on two independent sources: MarkTechPost (3 July 2026) and TestingCatalog, which links explicitly to the official URL. The Hugging Face model card returned a 401 and could not be read. I dropped the Jacobian conjecture claim: the author has not published the PDF yet, nor passed peer review.
- Incertezze
- The benchmark results and the previously unreported bugs are vendor claims: there are no independent replications and no peer-reviewed paper so far. Secondary sources disagree slightly on the active parameters (6 billion in the announcement and in most coverage, 6.5 billion according to TestingCatalog, which also adds a 256k context window I could not confirm) and on the date (2 July in the announcement, 3 July in the coverage). "Saturating" miniF2F means the benchmark no longer discriminates between models, not that the model proves any theorem. From here it is not possible to verify whether the 5 bugs were reported to and accepted by the respective maintainers.
- Perché pubblicarla
- This is a European release, with open weights and a permissive licence, in a field — formal proof — that closed and research-only models have dominated so far. It matters to readers on two fronts: technological sovereignty, since Mistral is Europe's leading operator, and software security, because the model does not stop at academic benchmarks but has found real defects in widely used open source libraries. It also complements rather than repeats our earlier pieces on Mistral, which dealt with industrial deals rather than technical capability.