Leanstral 1.5: Proof Abundance for All

Mistral AI · 2 weeks ago

Leanstral 1.5, a 6-billion-parameter open-source model, achieved 100% accuracy on miniF2F benchmarks and solved 587 of 672 PutnamBench problems while reaching 87% on FATE-H and 34% on FATE-X formal reasoning tasks. The model cost approximately $4 per problem solved, compared to $300 or more for competing systems like Seed-Prover. The wider availability of this free Apache-2.0 licensed model via Hugging Face and API enables automated bug discovery in real code repositories, uncovering 5 previously unknown bugs across 57 tested repositories.