Leanstral 1.5: Proof Abundance for All

Leanstral 1.5 is a free, Apache-2.0 licensed model with 6B active parameters designed to enhance formal verification and proof engineering in Lean 4. The model is trained using a three-stage process that includes mid-training, supervised fine-tuning, and reinforcement learning with CISPO in both multiturn and code agent environments. It achieves state-of-the-art results on several benchmarks, saturating miniF2F, solving 587/672 PutnamBench problems, and scoring 87% on FATE-H. Beyond benchmarks, Leanstral 1.5 has proven effective in real-world code verification by uncovering previously unknown bugs and is now openly available via Hugging Face and a free API.