Leanstral 1.5
Most models tell you they're right. This one hands you a proof.
What it is
Mistral's open-weights proof-engineering model for Lean 4 — a 119B-total / 6.5B-active MoE with 256K context that writes and repairs formal proofs and specifications. It saturates miniF2F, solves 587 of 672 PutnamBench problems, and surfaced five previously unknown bugs in real-world software-verification work.
Why it's interesting
Formal verification is the rare domain where a model's output can be machine-checked instead of taken on faith — and this one is plain Apache-2.0, both weights and code, from a lab with an inconsistent licensing history that got it right here.
Use cases
- Proving theorems and formalizing mathematics in Lean 4
- Writing and checking formal specifications for critical software
- Automated proof repair in CI pipelines
Who it's for
Formal-methods engineers, mathematicians, PL researchers
Setup
Advanced. vLLM ≥0.24 with tensor parallelism for self-hosting; Mistral's free hosted Labs endpoint covers experimentation until Sept 30, 2026
Limitations & cautions
A specialist, not an assistant — Lean 4 only. The 119B MoE still wants serious hardware to self-host, and the free hosted endpoint retires September 30, 2026.
Editorial takeaway
The quiet counterexample to 'you can't trust model output': here the compiler is the fact-checker, and it never gets tired.