Leanstral 1.5 targets Lean 4 theorem proving

Category: AI
Status: developing
Sources: model card, HN discussion
Summary: Mistral published Leanstral 1.5 on 2026-06-30, a model optimized for automated theorem proving and autoformalization in Lean 4. The model card lists 119B total parameters with 6.5B active (a mixture-of-experts configuration), a 256K token context window, and no-cost access. The page states no benchmark numbers.
Why it matters: A dedicated open formal-proof model extends LLM tooling into machine-checkable mathematics and verified-code workflows, where correctness is decidable rather than judged.
Follow-up: Watch for a technical report with miniF2F or Lean-benchmark results, weight availability and license, and adoption in proof-assistant tooling.