Leanstral targets proof engineering in Lean 4 repositories

Mistral introduced Leanstral on 16 March as an agent designed for Lean 4, a language and proof assistant used for formal mathematics and software specifications. The release included Apache 2.0 weights, a Vibe agent mode and an API endpoint. Its sparse architecture activates six billion parameters.

The company evaluated work in formal repositories, including completing proofs and defining mathematical concepts, rather than only solving isolated competition problems. Lean can check whether a proof follows its formal rules, which provides a different feedback signal from judging a fluent natural-language explanation. That does not remove the need to specify the right problem: a verified statement can still be narrower than a person intended. Leanstral’s proposed contribution is making work inside that formal workflow less manual.