Leanstral: Open-Source foundation for trustworthy vibe-coding
Summary
Mistral AI introduces Leanstral, the first open-source code agent designed for Lean 4, aimed at verifiable, high-integrity AI-assisted coding. The model uses a sparse 6B parameter architecture, is Apache-2.0 licensed, and offers zero-setup integration via Mistral Vibe with a free Labs API, plus an evaluation suite to benchmark proof engineering tasks. Benchmark data positions Leanstral as a cost-efficient, high-performance alternative to larger OSS models and Claude-family agents, with real-world case studies on Lean code reasoning and translation.