Mistral releases Leanstral 1.5, a small model built for Lean 4 theorem proving

Mistral AI released Leanstral 1.5 on June 30, 2026, a model specialized for automated theorem proving and autoformalization in the Lean 4 proof language. It has 119 billion total parameters, 6.5 billion active parameters and a 256,000-token context window.

The target is a narrow, hard problem: turning mathematical statements into machine-checkable Lean 4 proofs, a task general-purpose models handle poorly. By activating only 6.5 billion parameters per token, Leanstral is built to run cheaply relative to a dense model of similar reach.

Mistral says the model reaches a pass@2 score of 26.3 on its own benchmark, beating a comparison Claude Sonnet model by 2.6 points while costing $36 to run against $549 for that comparison. Those figures are Mistral’s own and have not been independently verified; the roughly 15-fold cost gap in particular depends on run conditions Mistral has not fully detailed. Leanstral is offered free on Mistral’s Labs tier through the console playground.

Formal theorem proving is a small but growing niche where correctness is verifiable by design – a Lean proof either checks or it does not – which makes it a cleaner testbed for reasoning models than open-ended benchmarks. A pass@2 of 26.3 also means the model still fails most problems on two attempts, so the result reads as early progress, not a solved task. Whether outside researchers reproduce the benchmark and cost claims will determine how much weight the numbers carry.