Models

← All models

Leanstral 1.5 119B A6B

Mistral AI · 2026-07-02 · 119.4B parameters

Leanstral 1.5 is Mistral AI's open-weight multimodal Lean 4 proof-engineering model, released as an update to Leanstral-2603 and trained through mid-training, supervised fine-tuning, and CISPO reinforcement learning for automated theorem proving, autoformalization, and code verification. Its 128-expert mixture-of-experts architecture routes four experts per token, accepts text and images, produces text, and provides optional `none`/`high` reasoning; Mistral describes it at rounded precision as 119B total and either 6B (launch post) or 6.5B (model card) active, and advertises a 256K context while recommending at most 200K for local serving.

Benchmark scores