Leanstral 1.5
Points and comments are a snapshot, not live.
Mistral AI released Leanstral 1.5, a 119B-parameter MoE model for Lean 4 formal proofs.
Leanstral 1.5 is a model optimized for automated theorem proving and autoformalization in Lean 4. It has 119B total parameters with 6.5B active, supports a 256k context window, and is available at no cost through Mistral's Labs program. It was released June 30, 2026, as an updated version of the earlier Leanstral model.
What commenters are saying
Commenters largely discussed Mistral's general utility rather than Leanstral specifically. Many use Mistral for tasks where it excels: creative writing (one described it as "bonkers weird" and "sassy"), OCR (called "off the charts good" by several), TTS/STT for French, and cost-effective coding. Multiple users cited EU data residency as a requirement for choosing Mistral over competitors. Several noted Mistral's models are competitive in specific narrow domains but lag behind frontier models on general benchmarks. One commenter linked to Curry-Howard correspondence to explain Lean's broader applicability to program specification.