Leanstral 1.5

Spec

Attribute	Value
Developer	Mistral AI
Released	2026-07-01 / 2026-07-02
Announced	2026-07-01 / 2026-07-02 (release blog post)
Context window	unknown
Pricing	free API endpoint (leanstral-1-5, Mistral Labs); open weights
License	Apache 2.0
Availability	HuggingFace weights + free API (leanstral-1-5) in Mistral Labs
Architecture	Mixture-of-Experts (MoE)
Total parameters	119B
Active parameters	~6.5B / token
Specialization	Lean 4 formal verification, theorem proving

Benchmarks

Benchmark	Score	Notes
miniF2F	100%	High school → math olympiad; full saturation
PutnamBench	587 / 672	Putnam competition problems (87.4%)
FATE-H	87%	Algebra, hard tier
FATE-X	34%	Algebra, expert tier

Use Cases

• Formal verification: generating Lean 4 proofs for functions and algorithms
• Automated theorem proving: mathematically rigorous derivations
• Agentic proof engineering: multi-step proof construction with tool use
• Real-world code verification: found 5 previously unknown bugs across 57 open-source repositories

Compared To

Mistral has not published a direct head-to-head comparison against other formal verification models (e.g., DeepSeek-Prover, Kimina-Prover). The 100% miniF2F score and 587/672 PutnamBench are best-in-class as of July 2026.

Why It Matters

Formal verification has historically required specialized expertise in proof assistants (Lean, Coq, Isabelle). A 6.5B active-parameter model that saturates miniF2F and discovers real bugs in production code dramatically lowers the barrier to deploying mathematically certified software. The Apache 2.0 license makes it commercially viable for aerospace, finance, and critical infrastructure.

Sources

• Mistral official blog: Leanstral 1.5: Proof Abundance for All — July 2026
• The Decoder
• sources/blogs/mistral-2026-07-02-leanstral-1-5.md

Open Questions

• How does Leanstral 1.5 compare to DeepSeek-Prover v2 and other dedicated formal-proof models?
• Does the model generalize beyond Lean 4 to other proof assistants (Coq, Isabelle)?
• Will Mistral release a fine-tuning recipe for domain-specific verification tasks?