Mistral's next specialist model is built for proof.
Mistral has built out a lineup of task-specific models — OCR, code, speech, safety — and now adds Leanstral 1.5, specialized in formal mathematical proof. The goal: hand off to AI the line-by-line verification work that researchers and engineers have long done by hand.
OCR, code, speech, safety
the one piece missing was "proof"
Mistral's specialist lineup had covered everything except formal mathematical proof.
For the past few years Mistral has favored a lineup of small, task-specific models over one enormous do-everything model. Document text extraction goes to Mistral OCR, code generation and agentic work to Codestral and Devstral, speech recognition and synthesis to Voxtral, and harmful-content detection to Moderation — each task handed to a model built for it. Now that lineup gains a model built specifically for formal proof: Leanstral 1.5.
"Formal proof" means writing a mathematical claim not as human intuition but in the grammar of an interactive theorem prover such as Lean 4, so that it can be checked mechanically, line by line. Traditionally that has been weeks or months of hand work for a mathematician. A compiler can judge each step as it's written, but coming up with that step has still been squarely a human job — which is why, unlike OCR or code generation, this was never an obvious task to simply "hand to AI."
| Domain | Model |
|---|---|
| OCR (document text extraction) | Mistral OCR |
| Code generation & agents | Codestral / Devstral |
| Speech recognition & synthesis | Voxtral |
| Harmful-content detection | Moderation |
| Formal mathematical proof | Leanstral 1.5 (new) |
Theorems no longer need
a human hand to check each line.
Generate, then verify —
run as a loop inside the model
What formal-proof AI shares is a built-in "grader": the compiler itself.
A general chat LLM's answer can only be judged, in the end, by whether it "sounds right" to a human. Formal-proof AI is different: the Lean 4 compiler can mechanically judge each step of a generated proof on the spot. A wrong step gets bounced back and the model tries another — this generate-and-verify cycle repeats until one goes through. With almost no room for ambiguity, it cuts out much of the manual work of eyeballing whether an answer is actually correct.
Mid-training
The model is trained on Lean 4 code and existing proof data to build a foundation in the proof language.
Supervised fine-tuning
It learns how proofs are actually structured from examples written by humans and prior models.
Reinforcement learning (CISPO)
Using the compiler's pass/fail signal, it is trained to construct proofs that actually go through on its own.
Per Mistral, Leanstral 1.5 was trained through these three stages: mid-training, supervised fine-tuning, then reinforcement learning with CISPO. Being able to use direct pass/fail feedback from a verifier — the compiler — is an advantage math has that open-ended natural-language tasks, with no single correct answer, don't.
Leanstral 1.5, by the numbers
Leanstral 1.5 saturates the miniF2F benchmark and solved 587 of 672 problems on PutnamBench, a set drawn from a university-level math olympiad. It also posts state-of-the-art scores on the harder FATE-H and FATE-X benchmarks, at 87% and 34% respectively. It ships under the Apache 2.0 license, with weights available to anyone on Hugging Face as well as a free API endpoint. In post-release testing it was also reported to have checked 57 open-source repositories and turned up five previously unknown bugs.
Useful only if proof-writing is part of your job
For everyday chat use, it will almost never come up.
Researchers & mathematicians
Drafting proofs and formalizing them into Lean 4 goes faster than by hand — useful for mechanically confirming a claim actually holds before peer review.
Finance quants
A good fit where the mathematical soundness of risk models or pricing logic needs formal backing — the kind of setting where an error becomes a direct loss.
General developers
For ordinary app development or chatbot work, there's almost no occasion to reach for Leanstral 1.5 — Codestral and Devstral remain the practical choice.
Why a niche launch still matters
Practical formal-proof AI has so far mostly lived in research projects like DeepMind's AlphaProof, making a generally available specialist model an unusual release. Apache 2.0 open weights plus a free API lowers the bar for university labs and financial verification teams to just try it. What to watch: which unsolved problems or software-bug hunts outside researchers pick up with Leanstral 1.5, and which domain Mistral extends its specialist-model strategy into next — physics simulation or circuit-design verification are plausible candidates.
At the same time, the formal-proof market stays small. The culture of writing proofs in Lean 4 is still confined to parts of the math and computer-science community, not something an ordinary dev team adopts overnight. High benchmark scores also only reflect performance on existing proof problem sets — they're no guarantee the model can prove a genuinely new, unsolved theorem on its own. Whether Mistral's strategy of stacking narrow specialist models keeps paying off will depend on real-world adoption from here.