Leanstral 1.5

Mistral's open-weight Lean 4 proof-engineering model: a 119B MoE activating 6.5B per token (128 experts, top-4) with 256K context, Apache-2.0. Works like a developer in a raw filesystem — edits files, runs bash, and queries the Lean language server for goals and type information — persisting through multiple rounds of context compaction on long-horizon proof tasks. Results: saturates miniF2F, solves 587/672 PutnamBench problems, and sets SOTA on FATE-H (87%) and FATE-X (34%). Mistral says it has already surfaced previously unknown bugs in open-source code via formal verification. Free in beta via the Labs API (`labs-leanstral-1-5`) and Mistral Vibe.