Leanstral 1.5: Proof abundance for all

Leanstral 1.5 achieves state-of-the-art formal verification results with an open-source, 6B parameter model.

Leanstral 1.5, an Apache-2.0 model with 119B total and 6B active parameters, saturates miniF2F (100%), solves 587/672 PutnamBench problems, and achieves 87% on FATE-H and 34% on FATE-X. It uses mid-training, supervised fine-tuning, and reinforcement learning with CISPO in multiturn and code agent environments. It uncovered 11 bugs (5 unreported) across 57 Rust repositories via a pipeline with Aeneas. Training cost ~$4 per PutnamBench problem vs. ~$300 for Seed-Prover 1.5 high setting. Weights and API are freely available.