Mistral releases Leanstral 1.5: 119B parameter open-source model for Lean 4 proof assistance
Mistral AI has released Leanstral 1.5, an open-source 119B parameter mixture-of-experts model designed specifically for Lean 4 proof assistance. The model features 128 experts with 4 active per token (6.5B activated parameters), a 256k token context window, and multimodal input capabilities.
Leanstral 1.5 119B A6B — Quick Specs
Mistral releases Leanstral 1.5: 119B parameter open-source model for Lean 4 proof assistance
Mistral AI has released Leanstral 1.5, an open-source 119B parameter mixture-of-experts model designed specifically for Lean 4, a proof assistant used for expressing complex mathematical objects and software specifications.
Technical specifications
Leanstral 1.5 is built as part of the Mistral Small 4 family and uses a mixture-of-experts architecture:
- Total parameters: 119B
- Active parameters per token: 6.5B (128 experts, 4 active)
- Context window: 256k tokens (200k recommended)
- Input: Text and images (multimodal)
- Output: Text only
The model supports a "reasoning effort" parameter with two settings: 'none' for standard operation and 'high' for chain-of-thought reasoning on complex prompts. Mistral recommends temperature 1.0 for inference.
Deployment and access
Leanstral 1.5 is available free through Mistral's API with no requirement for a Pro subscription. Users must opt into "Enable Labs models" in their Mistral account settings to access the model.
The model integrates with Mistral's Vibe CLI tool as a code agent, accessible via the command vibe --agent lean. According to Mistral, "Leanstral is capable of doing very long range tasks which requires hours of work."
For local deployment, Mistral recommends vLLM with specific configuration:
- Minimum vLLM version: 0.24.0
- Recommended tensor parallel size: 4
- Maximum model length: 200,000 tokens
- Attention backend: FLASH_ATTN_MLA
Integration with Lean ecosystem
The model works with the lean-lsp-mcp, a Model Context Protocol tool for AI agents to interact with Lean's language server. This enables the model to directly interact with Lean projects, prove theorems, and fix code within the Lean 4 environment.
Mistral recommends running the Vibe CLI inside VS Code's terminal and within Lean project directories for optimal workflow integration.
What this means
Leanstral 1.5 represents a specialized application of large language models for formal verification and mathematical proof assistance. The free API access removes cost barriers for researchers and developers working with Lean 4, while the mixture-of-experts architecture keeps inference costs manageable. The 256k context window enables the model to work with large codebases and complex proofs that require extensive context. This release positions Mistral as a key player in AI-assisted formal mathematics, an area that has traditionally relied on closed-source models or general-purpose coding assistants not optimized for proof systems.
Related Articles
Portugal releases Amália, open-source 9B parameter AI model trained on European Portuguese
Portugal has released Amália, its first national AI model trained specifically for European Portuguese. Built on EuroLLM-9B with 9 billion parameters, the model is fully open-source with weights, datasets, and code published under an open license. The government has committed €5.5m in initial funding through 2027.
DeepReinforce Releases Ornith-1.0, Open-Source Agentic Coding Model in 9B to 397B Sizes
DeepReinforce has released Ornith-1.0, an MIT-licensed model designed for agentic coding tasks with variants ranging from 9B to 397B parameters. Built on top of Apache 2.0-licensed Gemma 4 and Qwen 3.5 base models, the company claims it achieves state-of-the-art performance among open-source models of comparable size on coding benchmarks.
DeepSeek Releases V4-Pro with 1.6T Parameters, 1M Token Context at 27% Inference Cost of V3
DeepSeek has released two Mixture-of-Experts models: V4-Pro with 1.6 trillion parameters (49B activated) and V4-Flash with 284B parameters (13B activated), both supporting 1 million token context windows. V4-Pro requires only 27% of inference FLOPs and 10% of KV cache compared to V3.2 at 1M token context, trained on over 32 trillion tokens.
Mistral Releases Leanstral 1.5: 6B-Parameter Model Achieves 100% on miniF2F, Solves 587/672 PutnamBench Problems
Mistral AI released Leanstral 1.5, a free Apache-2.0 licensed model with 119B total parameters and 6B active parameters specialized for formal verification in Lean 4. The model achieves 100% on miniF2F benchmark, solves 587 of 672 PutnamBench problems at $4 per problem (versus $300+ for competitors), and reaches state-of-the-art 87% on FATE-H and 34% on FATE-X benchmarks.
Comments
Loading...