Leanstral, Mistral's open source code agent for Lean 4

Mistral AI releases Leanstral, a 6B-parameter open-source code agent for Lean 4 that formally proves its code under Apache 2.0 via the Mistral Vibe API.

Leanstral, published by Mistral AI, is presented as the first open-source code agent designed for Lean 4, a proof assistant capable of formalizing complex mathematical objects as well as software specifications. The underlying idea: rather than having a human review AI-generated code, which becomes a bottleneck as stakes rise, the agent formally proves that its implementation adheres to a strict specification. The human states what they want, the machine demonstrates it.

Where other proof systems wrap large generalist models or are limited to isolated problems, Leanstral focuses on efficiency, with a very parsimonious architecture of 6 billion active parameters, and on training in realistic formal repositories. It relies on Lean as a verifier and manages MCPs via the Mistral Vibe environment. According to Mistral, it rivals much larger models while costing significantly less.

The weights are released under the Apache 2.0 license, and the model is now accessible in Mistral Vibe, via a free API endpoint, or for download to run on one's own infrastructure. Mistral adds a technical report and a new evaluation suite, FLTEval.