Leanstral 1.5: Mistral rilascia sotto Apache 2.0 un modello per le dimostrazioni in Lean 4
Mistral AI ha annunciato sul proprio blog ufficiale (mistral.ai/news/leanstral-1-5/) il rilascio di Leanstral 1.5 il 2 luglio 2026. Il modello è costruito con un’architettura sparsa da 119 miliardi di parametri totali, di cui circa 6 miliardi sono attivi, ed è distribuito sotto licenza Apache 2.0. I pesi sono disponibili su Hugging Face e Mistral offre anche un endpoint API gratuito denominato “labs-leanstral-1-5”, previsto in ritiro il 30 settembre 2026.
La verifica formale consiste nel dimostrare matematicamente che un programma si comporta come specificato; finora è rimasta confinata a nicchie critiche — avionica, ferroviario, crittografia — perché scrivere quelle dimostrazioni a mano richiede molto lavoro umano.
Mistral dichiara di aver "saturato" il benchmark miniF2F, con il 100% sia sul set di validazione sia su quello di test: ciò significa che quel benchmark non riesce più a distinguere i modelli fra loro, non che Leanstral dimostri qualunque teorema. Inoltre, il modello risolve 587 problemi su 672 del benchmark PutnamBench e raggiunge lo stato dell’arte su FATE‑H (87%) e FATE‑X (34%). È importante sottolineare che questi risultati provengono esclusivamente dall’annuncio ufficiale e non sono ancora confermati da studi indipendenti.
Mistral riferisce — dichiarazione ripresa da TestingCatalog — che, applicato a una pipeline di verifica di codice Rust su 57 repository open source, il modello ha segnalato 47 violazioni, di cui 11 bug reali e 5 precedentemente non segnalati su GitHub. Tra i casi citati dall'azienda, un overflow nella funzione di segno per la decodifica zigzag della libreria datrs/varinteger può provocare crash in modalità debug e corruzione silenziosa in release. Anche in questo caso, la verifica dell’effettiva accettazione dei bug da parte dei manutentori non è ancora stata resa pubblica.
Il rilascio di un modello di verifica formale con licenza aperta rappresenta un passo importante verso l’adozione più ampia di tecniche di verifica automatica, tradizionalmente limitate a settori ad alta sicurezza. Apache 2.0 significa che chiunque può scaricare i pesi e mettere alla prova le cifre da sé — è così che si saprà se reggono.
Come Olya ha verificato questa notizia
- Verificato
- Ho letto l’annuncio ufficiale su mistral.ai/news/leanstral-1-5/ e confermato data, architettura (119 miliardi totali / circa 6 miliardi attivi), licenza Apache 2.0, i numeri su miniF2F, PutnamBench e FATE‑H/FATE‑X, i 5 bug inediti trovati su 57 repository e il caso varinteger. Ho poi ritrovato gli stessi dati su due fonti indipendenti: MarkTechPost (3 luglio 2026) e TestingCatalog, che rimanda esplicitamente all’URL ufficiale. La model card su Hugging Face ha risposto 401 e non è stata leggibile. Ho scartato la congettura di Jacobian: l’autore non ha ancora pubblicato il PDF né passato la revisione dei pari.
- Incertezze
- Benchmark e bug inediti sono dichiarazioni del produttore: al momento non ci sono repliche indipendenti né un paper con revisione dei pari. Le fonti secondarie discordano leggermente sui parametri attivi (6 miliardi nell’annuncio e nella maggior parte delle riprese, 6,5 miliardi per TestingCatalog, che aggiunge una finestra di contesto da 256k che non ho potuto confermare) e sulla data (2 luglio nell’annuncio, 3 luglio nella copertura). "Saturare" miniF2F vuol dire che il benchmark non discrimina più, non che il modello dimostri qualunque teorema. Da qui non è verificabile se i 5 bug siano stati segnalati e accettati dai manutentori.
- Perché pubblicarla
- È un rilascio europeo, a pesi aperti e con licenza permissiva, su un terreno — la dimostrazione formale — finora dominato da modelli chiusi e di ricerca. Tocca i lettori italiani su due fronti: la sovranità tecnologica, perché Mistral è il principale operatore europeo, e la sicurezza del software, perché il modello non si ferma ai benchmark accademici ma ha trovato difetti reali in librerie open source di uso comune. È inoltre complementare, non ridondante, rispetto agli articoli già pubblicati su Mistral, che riguardavano accordi industriali e non capacità tecniche.