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

_Lavora in Lean 4, dove ogni passaggio viene controllato da un compilatore. Mistral dichiara il 100% su miniF2F, punteggi sopra Claude Opus 4.6 a una frazione del costo e cinque bug inediti trovati in librerie Rust._

Fonte: https://andreapirazzini.it/blog/leanstral-1-5-mistral-dimostrazioni-matematiche · Andrea Pirazzini · 23 luglio 2026

## In breve

- Leanstral 1.5 è un agente di Mistral specializzato in dimostrazioni formali con Lean 4: 6 miliardi di parametri attivi, licenza Apache 2.0.
- Secondo Mistral risolve il 100% di miniF2F e sul test FLTEval supera Claude Opus 4.6 (43,2 contro 39,6) spendendo circa un settimo.
- Applicato a 57 repository Rust ha trovato 11 bug reali, 5 dei quali mai segnalati prima su GitHub.
- I pesi sono su Hugging Face, l'API è gratuita e l'agente si usa dentro Mistral Vibe; resta però uno strumento molto specialistico.

## 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.

- **100%** dei problemi di miniF2F risolti (sia in validazione sia in test)
- **6 miliardi** di parametri attivi, con licenza Apache 2.0
- **587** problemi di PutnamBench risolti (con 8 tentativi e 4 milioni di token)
- **5** bug mai segnalati prima, trovati in codice Rust (su 57 repository analizzati)

_Fonte: Mistral AI, luglio 2026_

## La scheda

| Voce | Cosa dichiara Mistral |
| --- | --- |
| Che cos'è | Un agente per dimostrazioni formali in Lean 4 |
| Architettura | Sparsa, con 6 miliardi di parametri attivi |
| Addestramento | Mid-training, fine-tuning supervisionato, apprendimento per rinforzo con CISPO |
| Licenza | Apache 2.0 |
| Pesi | Su Hugging Face |
| API | Gratuita, con il nome leanstral-1-5 |
| Dove si usa come agente | Mistral Vibe |
| Risultato di punta | 100% su miniF2F, sia validazione sia test |

## 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.

![Schema dell’addestramento: il modello riceve un teorema da dimostrare e propone una dimostrazione al verificatore; se viene respinta, l’errore torna al modello per un altro tentativo; se passa, o dopo troppi tentativi, l’esito va all’algoritmo CISPO](https://xfzvzyxtnexwldhdjrdj.supabase.co/storage/v1/object/public/blog-media/posts/265499c0-dd47-42ac-828f-2b916110d62d/e8a8f0e6-b748-434f-83f1-23562f6a4c63.webp)
*Il ciclo a più turni usato nell’apprendimento per rinforzo: a ogni tentativo è il compilatore di Lean a decidere se la dimostrazione regge. Schema: Mistral AI.*

## 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.

![Schema di una sessione in più turni: l’agente legge le istruzioni e i file del progetto Lean, interroga un server MCP, verifica il lavoro e manda un messaggio su Slack. A destra, Vibe collegato a filesystem, shell bash e server MCP](https://xfzvzyxtnexwldhdjrdj.supabase.co/storage/v1/object/public/blog-media/posts/265499c0-dd47-42ac-828f-2b916110d62d/b07e66ad-aeef-4e0d-bade-765a2f844062.webp)
*Leanstral dentro Vibe, turno dopo turno: legge il progetto, chiama strumenti e server MCP, verifica la dimostrazione e riferisce il risultato. Schema: Mistral AI.*

## 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.

| Benchmark | Risultato dichiarato | Cosa significa |
| --- | --- | --- |
| miniF2F | 100% su validazione e test | È il primo modello a risolverlo per intero |
| PutnamBench | 587 problemi (8 tentativi, 4 milioni di token) | 7 in più di Seed-Prover 1.5 high, a circa 4 $ a problema contro oltre 300 $ |
| FATE-H | 87 problemi | Nuovo record |
| FATE-X, livello dottorato | 34 problemi | Nuovo record |
| FLTEval | 43,2 (8 tentativi) | Sopra Claude Opus 4.6, fermo a 39,6, con un settimo della spesa |

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.

![Grafico a barre di Mistral. PutnamBench: Leanstral 1.5 risolve 587 problemi, dietro ad Aleph Prover e davanti a Seed-Prover 1.5 high, Goedel-Architect e AxProverBase. FATE-H: primo con 87. FATE-X: primo con 34, di poco davanti a Seed-Prover 1.5 high](https://xfzvzyxtnexwldhdjrdj.supabase.co/storage/v1/object/public/blog-media/posts/265499c0-dd47-42ac-828f-2b916110d62d/1cfc8ce3-5b9f-44b2-85b5-f4670a0474b0.webp)
*Su FATE-H e FATE-X Leanstral 1.5 è in testa; su PutnamBench, nel grafico di Mistral, un solo sistema risolve più problemi. Grafico: Mistral AI.*

### 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ù.

> **Nota:** Tutti i risultati di questo articolo sono pubblicati da Mistral. Sono verificabili in linea di principio, perché le dimostrazioni passano da un compilatore, ma al momento dell'annuncio non c'erano ancora riproduzioni indipendenti.

## 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.

**PutnamBench: problemi risolti** — Leanstral 1.5 con budget di token crescente per tentativo

| Voce | Valore |
| --- | --- |
| Budget minimo (50.000 token) | 44 |
| Secondo livello | 244 |
| Terzo livello | 493 |
| Budget massimo (4 milioni) | 587 |

_Fonte: dichiarato da Mistral AI, luglio 2026_

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.

**Dal codice Rust ai bug veri** — Cosa resta a ogni passaggio della pipeline

| Voce | Numero |
| --- | --- |
| Repository analizzati | 57 |
| Proprietà risultate violate | 47 |
| Bug reali confermati | 11 |
| Bug mai segnalati prima su GitHub | 5 |

_Fonte: dichiarato da Mistral AI, luglio 2026_

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.

| Configurazione | Costo | Punteggio FLTEval |
| --- | --- | --- |
| Leanstral 1.0, 1 tentativo | 18 $ | 21,0 |
| Leanstral 1.0, 2 tentativi | 36 $ | 26,3 |
| Claude Sonnet | 549 $ | 23,7 |
| Claude Opus 4.6 | 1.650 $ | 39,6 |
| Leanstral 1.5, 8 tentativi | circa 230 $ | 43,2 |

**FLTEval: punteggio** — Più alto è meglio

| Voce | Valore |
| --- | --- |
| Leanstral 1.0, 1 tentativo | 21 |
| Claude Sonnet | 23,7 |
| Leanstral 1.0, 2 tentativi | 26,3 |
| Claude Opus 4.6 | 39,6 |
| Leanstral 1.5, 8 tentativi | 43,2 |

_Fonte: dichiarato da Mistral AI, luglio 2026_

**FLTEval: quanto costa** — Dollari per eseguire l'intero test

| Voce | Valore |
| --- | --- |
| Leanstral 1.0, 1 tentativo | 18 $ |
| Leanstral 1.0, 2 tentativi | 36 $ |
| Leanstral 1.5, 8 tentativi | 230 $ |
| Claude Sonnet | 549 $ |
| Claude Opus 4.6 | 1.650 $ |

_Fonte: dichiarato da Mistral AI, luglio 2026 (230 $ è un valore approssimato)_

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.

![Grafico a linee di Mistral: punteggio percentuale su FLTEval con 1, 2 e 4 tentativi. La linea di Leanstral 1.5 è la più alta a ogni livello; sotto c’è Leanstral 1.0, poi Qwen3.5, Kimi K2.5 e GLM5](https://xfzvzyxtnexwldhdjrdj.supabase.co/storage/v1/object/public/blog-media/posts/265499c0-dd47-42ac-828f-2b916110d62d/675dc526-07c2-4983-ad17-22a4a0ac3474.webp)
*A ogni budget di tentativi Leanstral 1.5 resta sopra la versione precedente e sopra i modelli aperti messi a confronto. Grafico: Mistral AI.*

## 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:

```bash
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](https://andreapirazzini.it/blog/mistral-3-large-ministral-open-weight). 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](https://andreapirazzini.it/servizi/sistemi-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](https://andreapirazzini.it/guide/ai-locale-in-azienda).

## Cosa non si sa ancora

> **Attenzione:** Al momento dell'annuncio restano aperte alcune domande:
> 
> - come se la cava con altri proof assistant, come Coq, Isabelle o Agda;
> - se regge su repository industriali con milioni di righe di codice;
> - se la caccia ai bug funziona altrettanto bene con linguaggi diversi da Rust;
> - quanto costa davvero farlo girare in proprio: i parametri _attivi_ sono 6 miliardi, ma in memoria vanno tenuti tutti i 119 miliardi del modello, e l'annuncio non dice su quale hardware giri bene.

## 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

**Leanstral serve solo per la matematica?**

No. La pipeline di ricerca dei bug ha trovato 11 errori reali in repository Rust, quindi è utile anche per verificare codice di produzione. Resta comunque uno strumento specialistico, legato a Lean 4.

**Quanto costa usarlo?**

L'API è gratuita e i pesi sono pubblicati con licenza Apache 2.0, quindi si può anche eseguire in proprio senza pagare un servizio. Su FLTEval Mistral indica circa 230 $ per la 1.5 con otto tentativi; la prima versione, con un solo tentativo, ne costava circa 18.

**Come si confronta con Claude Opus?**

Su FLTEval Leanstral 1.5 ottiene 43,2 contro 39,6 di Opus 4.6, spendendo circa 230 $ invece di 1.650 $. Già la prima versione di Leanstral, con due tentativi, costava 36 $ e superava Claude Sonnet, che ne costa 549.

**Quanti parametri ha?**

6 miliardi di parametri attivi su 119 miliardi in totale, con un'architettura sparsa: il totale si ricava dal nome del modello su Hugging Face, Leanstral-1.5-119B-A6B.

**Si può usare dentro Mistral Vibe?**

Sì. Si installa Vibe con il comando uv tool install mistral-vibe, si configura la chiave API e si seleziona il modello leanstral-1-5.