Mistral AI ha rilasciato all'inizio di luglio 2026 Leanstral 1.5, un modello aperto specializzato in un compito che sembra astratto ma ha ricadute molto concrete: la verifica formale, cioè dimostrare in modo matematicamente rigoroso che un programma o un teorema si comportano esattamente come previsto. Lo strumento usa Lean 4, il linguaggio con cui matematici e ingegneri scrivono dimostrazioni che un computer può controllare passo per passo.
La particolarità è che si tratta di un modello open, distribuito con licenza permissiva Apache-2.0, e con risultati che secondo MarkTechPost lo collocano in cima al settore. Un modo per l'azienda europea di ritagliarsi una leadership in una nicchia ad alto valore, invece di inseguire i giganti sul terreno dei modelli generalisti.
Cosa sa fare: benchmark e cinque bug reali
I numeri sono notevoli. Leanstral 1.5 satura miniF2F, uno dei benchmark storici della dimostrazione automatica, e risolve 587 problemi su 672 di PutnamBench, una raccolta ispirata alla celebre competizione matematica statunitense Putnam. Ma il dato più interessante non è teorico: usato come agente per l'ingegneria delle dimostrazioni, il modello ha individuato cinque bug prima sconosciuti in repository open source reali. È la dimostrazione che la verifica formale non serve solo agli accademici, ma può scovare errori in software già in circolazione.
Sul piano tecnico, secondo la scheda ufficiale di Mistral, il modello attiva circa 6 miliardi di parametri su un totale di 119 miliardi (un'architettura a esperti, che accende solo la parte necessaria a ogni richiesta), offre una finestra di contesto da 256.000 token e accetta anche input testuali e immagini. L'addestramento ha previsto tre fasi, con una componente di apprendimento per rinforzo.
A cosa serve davvero la verifica formale
Per capire perché conta, basta pensare al software critico: sistemi avionici, dispositivi medici, protocolli crittografici, contratti finanziari automatizzati. In questi casi non basta «testare» il programma con qualche esempio, perché un solo caso non previsto può causare danni enormi. La verifica formale permette invece di provare, come un teorema, che il codice fa quello che deve fare in tutti i casi possibili. Il problema è che finora richiedeva competenze rarissime e tempi lunghissimi. Un modello capace di aiutare a scrivere queste dimostrazioni abbassa drasticamente la barriera.
Come provarlo, passo dopo passo
Leanstral 1.5 è accessibile in due modi principali, entrambi con un punto di ingresso gratuito.
- Tramite Hugging Face: i pesi del modello sono pubblicati sotto licenza Apache-2.0, quindi si possono scaricare ed eseguire sulla propria infrastruttura. Serve però hardware adeguato (GPU con parecchia memoria) e familiarità con l'ecosistema Lean.
- Tramite l'API di Mistral: è la via più semplice per iniziare senza gestire l'infrastruttura. Occorre creare un account sulla piattaforma di Mistral e generare una chiave API.
Un esempio minimo di chiamata all'API, in stile OpenAI-compatibile, per chiedere al modello di produrre una dimostrazione in Lean 4:
curl https://api.mistral.ai/v1/chat/completions \
-H "Authorization: Bearer $MISTRAL_API_KEY" \
-H "Content-Type: application/json" \
-d '{
"model": "leanstral-1.5",
"messages": [
{"role": "user", "content": "Dimostra in Lean 4 che la somma di due numeri pari e pari."}
]
}'Il modello restituisce un blocco di codice Lean 4 con la dimostrazione, che poi va compilato e verificato con il compilatore Lean per avere la certezza matematica che sia corretta. Chi vuole usarlo come agente su un intero progetto può collegarlo a un ambiente Lean e lasciarlo iterare: prova una strategia, legge l'errore del compilatore, corregge e riprova, fino a chiudere la dimostrazione.
Per iniziare a esplorare senza scrivere codice, il consiglio pratico è partire dall'API su un problema piccolo e ben definito, verificare l'output nel compilatore Lean, e solo dopo valutare se ha senso scaricare i pesi per un uso più intensivo. La documentazione completa, con nomi dei modelli e limiti, è sulla pagina ufficiale di Mistral.
Per chi ha senso oggi
Leanstral 1.5 non è uno strumento per l'utente medio: parla la lingua di chi lavora con dimostrazioni formali, matematica avanzata e software ad alta affidabilità. Ma proprio per questo è significativo. È il segnale che l'IA sta iniziando ad affrontare problemi dove non basta «sembrare» giusti: o la dimostrazione regge alla verifica del compilatore, oppure no. In un panorama in cui i modelli spesso producono risposte plausibili ma sbagliate, un sistema costretto a essere verificabile è una direzione preziosa — e il fatto che sia aperto e gratuito da provare lo rende accessibile a ricercatori e aziende di ogni dimensione.
C'è anche una lettura strategica. Mentre i grandi laboratori americani e cinesi si contendono il primato sui modelli generalisti, Mistral sceglie di piantare la bandiera su una nicchia verticale ma ad altissimo valore, dove la qualità conta più della notorietà. È una mossa tipica di chi non può competere sui volumi ma punta sull'eccellenza in un campo specifico, e per l'ecosistema europeo dell'IA è un tassello che vale la pena seguire: la verifica formale è esattamente il tipo di tecnologia che serve a rendere affidabili i sistemi critici su cui l'Europa vuole costruire la propria autonomia digitale.
