Mistral AI
·
4 months ago
Mistral released Small 4, a single model that combines text reasoning, image processing, and coding capabilities previously split across separate specialized models. The model has 119 billion total parameters with 6 billion active per token, a 256,000 token context window, and achieves 40% lower latency and 3 times higher throughput than its predecessor. Users can now deploy one versatile model instead of switching between separate systems for chat, reasoning, and coding tasks.
Mistral AI
·
4 months ago
Mistral released Leanstral, an open-source AI agent designed to generate and formally verify code in the Lean 4 proof assistant, addressing the bottleneck of human review in high-stakes software development. Leanstral achieves a score of 26.3 on the new FLTEval benchmark with two inference passes at a cost of $36, compared to Claude Sonnet's score of 23.7 at $549. The model is available free through Mistral Vibe, a free API endpoint, and under Apache 2.0 license for local use, enabling developers to use formally verified code generation without manual proof checking.
