Mistral vydal Leanstral 1.5 — open-source model pre formálne dôkazy rieši 87 % PutnamBench problémov
Mistral AI vydal Leanstral 1.5, open-source (Apache-2.0) model špecializovaný na formálne dôkazy v Lean 4. So 119B celkovými a len 6B aktívnymi parametrami dosahuje 100 % na miniF2F a vyrieši 587 z 672 PutnamBench matematických problémov.