Summary
Leanstral 1.5 is a 119-billion-parameter open model from Mistral, available free via the Mistral API, built specifically to write formally verified proofs in Lean 4. Fahd Mirza walks through the model end-to-end on Ubuntu using Mistral Vibe CLI — starting from a trivial hello-world proof (adding zero to a natural number) and progressing to multi-step algebraic reasoning that requires genuine intermediate steps rather than one-word shortcuts.
What differentiates Leanstral from general-purpose coding models is its verifier loop: the model writes a candidate proof, submits it to the Lean 4 compiler — an impartial judge that either accepts or rejects — and if rejected, receives the error output and retries until the compiler signs off or runs out of attempts. This means every proof shown to the user has already passed a formal checker, not just a plausibility filter. Mistral reports that in testing on real-world projects, Leanstral caught bugs that comprehensive test suites had missed entirely, because tests only cover cases a developer anticipated.
The video also covers Leanstral’s architecture as a full development agent: it has access to the file system, a bash shell, and external tools via MCP, allowing it to operate like a developer at a keyboard rather than a question-answering system. For engineers working on safety-critical software, or anyone curious about formal verification as an alternative to probabilistic testing, this video provides a clear, practical introduction to state-of-the-art proof generation with a free open-weight model.
📺 Source: Fahd Mirza · Published July 04, 2026
🏷️ Format: Review
