Open Models and Developer Tooling Updates #68
Today's Letter
Mistral, Leanstral 1.5 for Lean 4 released
- Mistral AI released Leanstral 1.5, a free Apache-2.0 licensed model for proof engineering in Lean 4.
- The model has 119B total parameters with 6B active parameters, positioning it as an open model focused on formal verification workloads.
- Mistral says Leanstral 1.5 saturates miniF2F, solves 587 of 672 PutnamBench problems, and reaches 87% on FATE-H and 34% on FATE-X.
- Training used three stages: mid-training, supervised fine-tuning, and reinforcement learning with CISPO.
- The RL setup includes a multiturn theorem proving loop with Lean compiler feedback and a code-agent environment that edits files, runs bash commands, and uses the Lean language server.
- Beyond benchmark results, Mistral says the model found five previously unknown bugs across 57 tested open-source repositories.
- The release is fully open-sourced and is available through Hugging Face and a free API for practical proof engineering use.
Source: mistral.ai
DeepSeek, V4 Preview with 1M Context Released
- DeepSeek announced DeepSeek-V4 Preview on April 24 and said the release is live, open-sourced, and available through both chat and API endpoints
- The lineup includes DeepSeek-V4-Pro with 1.6T total parameters and 49B active parameters, and DeepSeek-V4-Flash with 284B total parameters and 13B active parameters
- DeepSeek set 1M context as the default across its official services and said both V4 models support Thinking and Non-Thinking modes
- The API requires only a model switch to `deepseek-v4-pro` or `deepseek-v4-flash`, while keeping the existing base URL, and supports both OpenAI Chat Completions and Anthropic-compatible APIs
- DeepSeek described a new attention design based on token-wise compression and DeepSeek Sparse Attention, aimed at reducing long-context compute and memory cost
- The company said V4 is integrated with agent tools including Claude Code, OpenClaw, and OpenCode, and is already used for in-house agentic coding workflows
- DeepSeek also said `deepseek-chat` and `deepseek-reasoner` will be fully retired after July 24, 2026, 15:59 UTC; they currently route to DeepSeek-V4-Flash in non-thinking and thinking modes
- Open weights and a technical report were published through Hugging Face alongside the release
Source: api-docs.deepseek.com
More: github.com · theregister.com
Jocoletter curates AI, software, and product trends for developers and builders.
#DeepSeek #Mistral