Leanstral 119B model beats proprietary provers, open‑source theorem proving goes mainstream
Leanstral, a 119‑billion‑parameter, open‑source code‑agent for Lean 4, solves 587 of 672 miniF2F problems and sets a new state‑of‑the‑art 34 % on FATE‑X, matching or surpassing far larger closed models. Its general‑purpose Mistral Vibe interface lets users run it like any coding assistant, lowering compute cost tenfold and uncovering real‑world bugs.