Mistral AI released Leanstral 1.5, a 6-billion-parameter model for formal proof engineering in Lean 4, under an Apache-2.0 license. It is trained via a three-stage pipeline (mid-training, supervised fine-tuning, and reinforcement learning using CISPO) across two RL environments covering iterative theorem proving and agentic code manipulation. The model fully saturates the miniF2F benchmark, solves 587 of 672 Putnam competition problems, and reaches 87% on advanced algebra benchmarks. Mistral also reports the model independently found five previously unknown bugs in real-world code repositories, showing formal verification applied beyond pure theorem-proving.
