Leanstral 1.5: dimostrazioni in abbondanza per tutti

Leanstral 1.5 is a free, open-source model with 6B active parameters designed for formal verification and proof engineering in Lean 4. Trained using a three-stage process including reinforcement learning, it achieves state-of-the-art results on benchmarks like miniF2F, PutnamBench, and FATE-H/X. The model demonstrates strong capabilities in practical code verification, proving time complexity for data structures like AVL trees. It has also been used to automatically discover previously unknown bugs in open-source Rust repositories by generating and attempting to prove correctness properties.