Mistral Releases Leanstral

Mistral has released Leanstral, the first open-source code agent for Lean 4 with 6B active parameters, designed for formal proof engineering in realistic repositories rather than isolated math problems. It outperforms much larger open-source models on the new FLTEval benchmark while being significantly more efficient, and supports MCP integration through Mistral's vibe platform under an Apache 2.0 license.