Lean 4 macht mathematische Sätze und Software-Spezifikationen maschinenprüfbar. Leanstral 1.5 aktiviert vier von 128 Experten pro Token und ist über Hugging Face, einen kostenlosen API-Endpunkt sowie Mistral Vibe verfügbar.
Mistral nennt 100 Prozent auf miniF2F, 587 von 672 Aufgaben auf PutnamBench sowie 87 Prozent auf FATE-H und 34 Prozent auf FATE-X. Diese Benchmarkwerte sind Anbieter-Eigenmessungen. In einem separaten Verifikationstest fand das Modell laut Mistral fünf bisher unbekannte Fehler in 57 Open-Source-Repositories, darunter einen kritischen Überlauf in einer Vorzeichenfunktion.
Die harte Prüfung eines Lean-Beweises unterscheidet die Anwendung von gewöhnlichen Text- oder Coding-Benchmarks. Dennoch stammen auch die Repository-Funde aus Mistrals eigener Untersuchung. Unabhängige Reproduktionen der Benchmarks und der realen Fehlerfunde stehen aus.