A Mistral kiadta a Leanstral 1.5 modellt, egy nyílt forráskódú, Apache-2.0 licenc alatt elérhető formális matematikai és kódverifikációs rendszert. A modell 119 milliárd paraméterből áll, ám mindössze 6 milliárd aktív paraméterrel működik — ez jelentősen csökkenti a futtatási költségeket a teljes méretű modellekhez képest.
A Leanstral 1.5 teljesítménye a matematikai benchmarkokon kiemelkedő: 100 százalékot ér el a miniF2F teszten, a 672 PutnamBench problémából 587-et megold, és új rekordokat állít a FATE-H (87 százalék) és FATE-X (34 százalék) absztrakt algebra benchmarkokon. A MathArena mérései szerint a teljesítménye eléri a GPT-5.5 xhigh szintjét, ami figyelemre méltó eredmény egy nyílt súlyú modelltől.
A modell képességei nem korlátozódnak a matematikai bizonyításokra: 57 tesztelt kód repository-ban 47 sérülékenységet talált. A rendszer ingyenes API-n és HuggingFace-en keresztül is elérhető, a forráskód és a súlyok teljes egészében nyíltak.
