Mistral releases Leanstral, an open-source coding agent for Lean 4
Mistral has released Leanstral, which it calls the first open-source coding agent for Lean 4. It uses a sparse architecture with 6B active parameters; weights are available under Apache 2.0, and the agent is integrated into Mistral Vibe and the free `labs-leanstral-2603` API endpoint.
Why it matters: Mistral has open-sourced a Lean 4 coding agent and reports cost and score comparisons with Claude models and open models, helping readers assess the value of formal-verification approaches.

