Leanstral 1.5: Proof Abundance for All

What happened

Mistral AI released Leanstral 1.5, an updated open-source (Apache-2.0) model for formal proof engineering in Lean 4. Available on Hugging Face and as a free API endpoint on Mistral Labs.

Context and impact

Formal software verification matters for safety-critical systems and mathematical research. Leanstral 1.5 saturates the full miniF2F dataset (100%) and solves 587 of 672 PutnamBench problems — a new state-of-the-art for automated theorem proving. It also discovered five previously unknown bugs across 57 open-source repositories and proved time-complexity guarantees for AVL tree implementations.

Details

• Parameters: 119B total, 6B active (MoE architecture)
• Context: 256k tokens
• License: Apache 2.0, weights on Hugging Face
• miniF2F: 100% (fully saturated)
• PutnamBench: 587/672 (87%)
• FATE-H: 87%, FATE-X: 34% (high school / graduate algebra)
• Real-world: 5 new bugs found in 57 repositories
• Access: free via Mistral Labs API (leanstral-1-5)