Leanstral 1.5, l'agente di Mistral che scrive dimostrazioni matematiche controllate dal compilatore

Perché se ne parla#

I modelli linguistici hanno un difetto noto a chiunque li usi: possono sbagliare con grande sicurezza. In matematica e nel software critico questo è un problema serio, perché una dimostrazione "quasi giusta" è semplicemente sbagliata.

Leanstral 1.5, rilasciato da Mistral AI, prende la strada opposta. Non chiede di fidarsi: scrive le sue dimostrazioni in Lean 4, un linguaggio in cui ogni passaggio viene controllato da un programma. Se la dimostrazione passa il controllo è corretta, se non lo passa l'agente ci riprova. Mistral lo presenta come il primo modello open source nato apposta per questo lavoro, non un modello generico adattato.

I numeri dichiarati sono notevoli: 100% su miniF2F, nuovi record su FATE-H e FATE-X, un punteggio superiore a Claude Opus 4.6 su FLTEval con una spesa molto più bassa. E un risultato che interessa anche fuori dalla matematica: usato per controllare codice Rust, ha trovato bug veri che nessuno aveva ancora segnalato.

La scheda#

Prima di tutto: cos'è Lean e perché cambia le regole#

Lean 4 è un proof assistant: un linguaggio in cui si scrivono oggetti matematici, teoremi e anche specifiche di software, e un programma (il compilatore) verifica che ogni passaggio sia logicamente valido. Pensatelo come un revisore instancabile e pignolo, che mette il timbro solo se tutto torna fino all'ultima virgola.

Per un modello AI questa è una condizione ideale. Di solito il problema è capire se la risposta è giusta; qui la risposta arriva gratis e senza margini di errore, perché è il compilatore a dirlo. Mistral lo definisce un verificatore perfetto: l'agente può tentare, sbagliare e correggersi quante volte vuole, ma alla fine consegna solo ciò che il compilatore ha accettato.

Il punto che distingue Leanstral dai sistemi precedenti, secondo Mistral, è il terreno di gioco. Molti strumenti di dimostrazione automatica avvolgono un modello generalista, oppure lavorano solo su esercizi isolati. Leanstral invece è pensato per muoversi dentro repository formali veri, con tanti file, definizioni che dipendono l'una dall'altra e lemmi da costruire strada facendo.

Come è stato addestrato#

L'addestramento è passato da tre fasi: un mid-training, un fine-tuning supervisionato e infine l'apprendimento per rinforzo con una tecnica chiamata CISPO. In quest'ultima fase il modello ha fatto pratica in due ambienti diversi.

• Il ciclo a più turni. Riceve un teorema, propone una dimostrazione, legge la risposta del compilatore e corregge. Va avanti così finché la dimostrazione compila o finché non esaurisce il budget a disposizione.

• L'ambiente da sviluppatore. Qui si comporta come un programmatore dentro un filesystem reale: apre e modifica file, lancia comandi bash e interroga il language server di Lean, che gli mostra in tempo reale obiettivi ancora aperti, errori e informazioni sui tipi.

Non un completamento, un agente#

La differenza con un normale modello che "completa il testo" è netta. L'agente Leanstral:

• esplora i repository per capire cosa c'è già;

• costruisce lemmi di supporto, cioè risultati intermedi che servono per arrivare al teorema finale;

• resiste a più compattazioni del contesto: quando la conversazione diventa troppo lunga riassume il lavoro fatto e prosegue senza perdere il filo;

• viene controllato da SafeVerify, che conferma la correttezza rispetto ai teoremi che andavano dimostrati.

Tramite Vibe può usare qualunque server MCP, lo standard con cui un agente si collega a strumenti esterni, ed è stato addestrato in particolare per rendere al meglio con lean-lsp-mcp, il collegamento al language server di Lean.

I risultati sui benchmark#

Mistral misura Leanstral 1.5 su cinque prove, che vanno dagli esercizi di base fino a problemi da dottorato di ricerca.

Nel materiale di lancio Mistral affianca a questi numeri un grafico che mette Leanstral 1.5 a confronto con altri sistemi di dimostrazione automatica su PutnamBench, FATE-H e FATE-X.

Cosa vuol dire "8 tentativi"#

Nelle tabelle compare spesso la sigla pass@k: il modello ha k tentativi e il problema conta come risolto se almeno uno va a buon fine. In molti ambiti va letto con cautela, perché nella vita reale non si sa quale dei tentativi sia quello giusto. In Lean invece lo si sa: il compilatore scarta quelli sbagliati. Per questo, qui, più tentativi sono un modo legittimo di spendere di più per ottenere di più.

Più tempo gli si dà, più risolve#

Uno dei dati più interessanti riguarda il test-time scaling, cioè cosa succede quando si concede al modello più "tempo per pensare", misurato in token per tentativo. Su PutnamBench, passando da 50.000 a 4 milioni di token, i problemi risolti salgono sempre: 44, poi 244, poi 493, infine 587. Mistral lo descrive come il miglior andamento mai visto per un modello di ragionamento formale.

Tradotto: invece di arrendersi, l'agente continua a ragionare, a modificare file e a rivedere il lavoro anche per milioni di token. Per chi lo usa significa poter scegliere quanto spendere in base a quanto è importante il risultato.

Dal teorema al codice: due casi concreti#

La matematica pura è solo metà della storia. Lean serve anche a dimostrare che un programma fa esattamente quello che deve, e qui Mistral porta due esempi.

Alberi AVL: dimostrata la velocità#

Gli alberi AVL sono una struttura dati classica, usata per tenere in ordine grandi elenchi e trovarli in fretta. La loro promessa è che le operazioni richiedano un tempo proporzionale al logaritmo del numero di elementi, in sigla O(log n). Leanstral ha dimostrato formalmente questa garanzia per un'implementazione reale.

Non è stato un lavoro breve: 2,7 milioni di token e 22 compattazioni del contesto. Ha richiesto un'induzione strutturale che seguisse la forma ricorsiva dell'albero, un conteggio attento del tempo di esecuzione dentro la struttura monadica del codice e l'esame di tutti i casi possibili di ribilanciamento.

Caccia ai bug nel codice Rust#

Il secondo esperimento è quello che più interessa a chi scrive software. Una pipeline automatica ha preso codice Rust, lo ha tradotto in Lean con lo strumento Aeneas, ha generato le proprietà che il codice avrebbe dovuto rispettare e ha provato a dimostrarle. Quando una dimostrazione fallisce, è un indizio che il codice non si comporta come dovrebbe.

Un esempio concreto: nella libreria datrs/varinteger, la funzione sign usata per la decodifica zigzag andava in overflow. Il calcolo Std.U64.MAX + 1 supera il numero più grande rappresentabile: nella versione di debug il programma si blocca, in quella di produzione prosegue con un valore sbagliato senza avvisare nessuno. È il tipo di errore peggiore, perché non si vede.

Quanto costa rispetto a Claude#

Il confronto economico è fatto su FLTEval. Ecco i dati pubblicati da Mistral: accanto alla 1.5 ci sono i risultati della prima versione, Leanstral 1.0.

Qualche conto per leggere bene la tabella:

• 230 $ contro 1.650 $ vuol dire circa un settimo della spesa, per un punteggio più alto (43,2 contro 39,6).

• Con due tentativi Leanstral spende 36 $ e batte Sonnet, che ne costa 549: circa quindici volte meno.

• Mistral cita anche un rapporto di 92 volte rispetto a Opus. Il numero torna confrontando Opus con la configurazione a un solo tentativo (1.650 diviso 18); con due tentativi il divario scende a circa 46 volte.

Nella tabella di Mistral le prime due righe sono indicate solo come "Leanstral", senza numero di versione; la riga a otto tentativi è quella espressamente attribuita alla 1.5.

Un secondo grafico di Mistral mostra come sale il punteggio su FLTEval con più tentativi, mettendo a confronto le due versioni di Leanstral e alcuni modelli aperti.

Come provarlo#

Leanstral 1.5 si può usare in tre modi:

• scaricando i pesi da Hugging Face, con licenza Apache 2.0, per farlo girare in proprio;

• attraverso l'API gratuita, chiedendo il modello leanstral-1-5;

• come agente dentro Mistral Vibe, che lo integra in modo nativo.

Per Vibe l'installazione indicata da Mistral è questa:

uv tool install mistral-vibe && vibe --setup

Dopo la configurazione si inserisce la chiave API e si sceglie il modello leanstral-1-5.

Un'avvertenza pratica: Leanstral non lavora da solo. Serve un ambiente Lean installato e funzionante, perché è il compilatore a fare da giudice.

Punti forti e limiti#

Cosa convince#

• È addestrato apposta per le dimostrazioni formali, non è un modello generico adattato.

• Risolve il 100% di miniF2F.

• Su FLTEval supera Opus 4.6 con circa un settimo della spesa.

• È un agente vero: lavora nel filesystem, lancia comandi, dialoga con il language server di Lean.

• Ha trovato cinque bug inediti in repository Rust reali.

• Licenza Apache 2.0 e API gratuita: nessuna barriera per provarlo.

• I risultati crescono senza interruzioni passando da 50.000 a 4 milioni di token.

Dove si ferma#

• È uno specialista: fuori da Lean 4 e dalla matematica formale non è pensato per competere.

• Su PutnamBench arriva a 587 problemi su 672, circa l'87%: la prova più difficile non è ancora esaurita.

• Senza un'installazione di Lean non funziona.

• Le prestazioni su codice diverso dal percorso da Rust a Lean non sono state misurate.

• Per ora i numeri vengono tutti dal produttore.

Cosa significa per un'azienda#

Per la maggior parte delle PMI Leanstral non è uno strumento da usare domani mattina: non scrive email, non riassume contratti, non risponde ai clienti. Per quei lavori Mistral ha modelli generalisti, come quelli della famiglia Mistral 3. Il suo pubblico sono i gruppi di ricerca, chi sviluppa software dove un errore costa caro (pagamenti, sistemi embedded, librerie crittografiche) e le software house che vogliono aggiungere un livello di controllo in più.

C'è però un'idea che vale per tutti. L'AI diventa affidabile quando il suo lavoro passa da un controllo automatico che non si lascia convincere. In Lean quel controllo è il compilatore; in un progetto aziendale può essere una regola di validazione, un confronto con il gestionale, un'approvazione umana nei punti critici. Progettare questi controlli è metà del lavoro quando si costruisce un sistema AI su misura.

E c'è un dettaglio da non sottovalutare: con licenza Apache 2.0 e pesi pubblici, Leanstral si può far girare sui propri server, senza mandare codice riservato a un servizio esterno. Se il tema vi interessa, ne parlo nella guida all'AI locale in azienda.

Cosa non si sa ancora#

Il mio parere#

Leanstral 1.5 mi sembra uno dei rilasci più intelligenti di quest'estate, per tre motivi. È un modello open source addestrato apposta per le dimostrazioni formali, non un modello generico con un'interfaccia sopra. Ottiene risultati migliori di Opus 4.6 su FLTEval spendendo circa un settimo. E la caccia ai bug in Rust mostra che l'utilità non si ferma alla matematica astratta.

Quello che mi convince di più, però, è il principio: un modello che non chiede fiducia, perché ogni suo risultato passa da un controllo che non si può aggirare. È la direzione giusta per chi vuole usare l'AI in lavori dove sbagliare costa. Resta uno strumento per specialisti, e i numeri, per quanto verificabili in teoria, aspettano ancora conferme indipendenti.

Domande frequenti#