Leanstral 1.5: Democratizing Proof Abundance

Date: July 2, 2026 | Author: Leanstral Team at Mistral AI | Read Time: $\approx 6$ minutes

Executive Summary: Leanstral 1.5 is a free, Apache-2.0 licensed model featuring $119\text{B}$ total parameters (with only $6\text{B}$ active). It represents a quantum leap in formal verification, achieving total saturation of miniF2F, solving $587/672$ PutnamBench problems, and setting new SOTA records on FATE-H ($87\%$) and FATE-X ($34\%$).

---

🚀 Overview

Mistral AI is evolving the landscape of formal verification. While the original Leanstral introduced a practical path for proof engineering in Lean 4, the new Leanstral 1.5 makes these capabilities more potent and accessible.

Beyond mere benchmarks, this model demonstrates real-world utility by verifying intricate code properties and identifying hidden 5 previously unknown bugs across 57 different open-source repositories.

---

🛠️ The Training Pipeline

The development of Leanstral 1.5 followed a rigorous three-tier methodology:

RL Environment Specialization

The model was honed in two distinct Reinforcement Learning (RL) settings:

1. The Multiturn Environment: A feedback loop where the model attempts to prove or disprove a theorem.
   • Process: Submit Proof $\rightarrow$ Receive Lean Compiler Feedback $\rightarrow$ Refine.
   • Success Condition: The proof must successfully compile.
2. The Code Agent Environment: The model acts as a software engineer with direct filesystem access.
   • It utilizes bash commands and the Lean language server to monitor goals and type errors.
   • It handles "long-horizon" tasks, such as constructing auxiliary lemmas.

Agentic Workflow Checklist:

• Edit source files
• Execute shell commands
• Inspect real-time goals/errors
• Perform context compaction
• Final verification via SafeVerify fork

Example of an agentic command:

# Leanstral agent checking for compilation errors in a lemma
lean --make src/Theorem_Proof.lean

---

📊 Evaluation & Benchmarks

Leanstral 1.5 was tested against several high-difficulty mathematical benchmarks:

Comparative Analysis

When compared to other provers (without natural-language hints), Leanstral 1.5 outperforms Goedel-Architect, AxProverBase, and Seed-Prover 1.5 (high).

The Cost Efficiency Gap: The most striking difference is the economic cost per problem solved:

• Leanstral 1.5: \approx \4$
• Aleph Prover: \approx \54 - $68$
• Seed-Prover 1.5 (high): ~~\300+$~~ (Estimated based on$10 \text{ H20-days}$ per problem)

---

🔓 Availability

Leanstral 1.5 is fully open-sourced to encourage the growth of the formal verification community. It can be accessed via:

• Hugging Face (Model weights)
• Free API (Direct inference)

By combining efficiency with rigor, Leanstral 1.5 ensures that the future of mathematical proof engineering is not just powerful, but abundant for all.