Leanstral 1.5 publishes theorem-proving benchmarks and reports repository bug finds

Category: AI
Status: developing
Sources: Mistral blog, HN discussion
Summary: Mistral's Leanstral 1.5 blog post (2026-07-02) adds benchmark numbers to the Lean 4 theorem-proving model covered on 2026-07-01, when only the model card was available. The company reports the model saturates miniF2F at 100 percent on validation and test, solves 587 of 672 PutnamBench problems, and reaches state-of-the-art figures on FATE-H (87 percent) and FATE-X (34 percent), and states it uncovered 5 previously unknown bugs across 57 tested repositories through automated verification workflows. The model is 119B total parameters with about 6B active, Apache-2.0, with weights on Hugging Face and a free leanstral-1-5 API endpoint. The benchmark figures are the vendor's own.
Why it matters: Machine-checkable formal proving is a domain where model output is verifiable rather than judged, so measured gains on Lean benchmarks and real-repository bug finds are stronger signal than typical benchmark claims, pending independent reproduction.
Follow-up: Track independent reproduction of the miniF2F and PutnamBench results and confirmation of the reported repository bug findings.