Leanstral 1.5
119B MoE (128 experts, 4 active, ~6B active params). Update of Leanstral (Leanstral-2603, March 16, 2026). 256K context, ≤200K recommended.
- Context window
- 256,000 tokens
- Input
- text
- Output
- text
- License
- apache-2.0
- Pricing
- input: $0 · output: $0 (free API endpoint (per Mistral's announcement)) source
- Verified
- 2026-10-01
How to call it
| Provider | Model id | Endpoint / URL | Docs |
|---|---|---|---|
| Mistral API | leanstral-1-5 | https://api.mistral.ai/v1/chat/completions | docs |
| Hugging Face | — | huggingface.co/mistralai/Leanstral-1.5-119B-A6B | — |
Notable capabilities (2)
- Lean 4 proof agent: Specialised for Lean 4 theorem proving in real repositories: miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34% (Mistral-reported). source
- Formal code verification: Used as a verification agent over 57 open-source repos, it found 5 previously unreported bugs (e.g. an integer overflow in datrs/varinteger). source
Open-weights Lean 4 prover and verification agent from Mistral. Weights are on Hugging Face (Apache 2.0), and Mistral's API offers a free endpoint (leanstral-1-5).
Timeline entry
- Mistral releases Leanstral 1.5, an open-weights Lean 4 proof agent that saturates miniF2F and solves 587/672 PutnamBench problems ★★★
On July 2, 2026 Mistral released Leanstral 1.5 ("Proof abundance for all"), an Apache-2.0, 119B-parameter (6B active) MoE model specialised for Lean 4 theorem proving and code verification. It updates the original Leanstral of March 16, 2026. Mistral reports 100% on miniF2F, 587 of 672 PutnamBench…
Other Mistral AI models
Mistral OCR 4.1 · Mistral Medium 3.5 · Voxtral TTS · Mistral Small 4 · Voxtral Transcribe 2 (Mini Transcribe V2 + Voxtral Realtime) · Mistral Large 3 · Codestral 25.08 · Voxtral Small · Robostral Navigate