Mistral AI

Backlink: 2026 04 14 Mistral latest model

Mistral AI is a developer of large-language-models specializing in open-weight architectures.

Model Portfolio

mistral 3 large

• Architecture: mixture-of-experts (MoE)
• Parameters: 675B
• License: apache-20 (Open Source)
• Capabilities: State-of-the-art non-reasoning model.
• Benchmarks: Competes closely with DeepSeek V3 and kimi-k2.

Leanstral 1.5

• Focus: Formal Verification and code correctness proving in Lean 4.
• Architecture: 119B parameters, 6B active (A6B).
• License: Free and Open Source.
• Capabilities: Specialized for writing formal proofs; distinct from general-purpose generation models.
• Source: Leanstral 1.5: AI for Formally Proving Code Correctness in Lean 4

References

• Mistral 3 Large: Model Review & Testing
• Leanstral 1.5: AI for Formally Proving Code Correctness in Lean 4

Source Notes

• 2026-04-07: Benchmarking SLMs Identifying 4GB General Problem Solving Champions · ▶ source
• 2026-04-10: Marc Benioff Salesforces AI Strategy Agents Slack and Work · ▶ source
• 2026-04-21: Local Mistral · ▶ source
• 2026-07-05: Leanstral 1.5: AI for Formally Proving Code Correctness in Lean 4 · ▶ source