Post #3564629
2026-03-17 10:29 UTC
Really nice vibe-proving model open-sourced by Mistral!
Leanstral is a code agent designed for Lean 4. Leanstral is designed to be highly efficient (with 6B active parameters) and trained for operating in realistic formal repositories.
Mistral also published a new evaluation suite, FLTEval, to move evaluations beyond their focus on competition math. Evaluation shows that Leanstral can translate between Rocq and Lean successfully!
https://mistral.ai/news/leanstral
Replies (1)
-
@fj@mastodon.social 2026-07-03 19:45
Leanstral 1.5, a free Apache-2.0 licensed model with 6B active parameters, delivers a major performance upgrade in formal verification, saturating miniF2F, solving 587/672 PutnamBench problems, and achieving state-of-the-art results on FATE-H (87%) and FATE-X (34%). Fully open-sourced and available via Hugging Face and a free API, Leanstral 1.5 is now accessible for practical proof engineering in Lean 4. https://mistral.ai/news/leanstral-1-5/