Nel 2024, le Olimpiadi Internazionali della Matematica sono state testimoni di una pietra miliare storica. Sebbene la competizione sia tradizionalmente una battaglia di ingegno tra gli studenti più brillanti del mondo, un concorrente non ufficiale ha rubato i riflettori: AlphaProof di Google DeepMind. Il programma di intelligenza artificiale ha ottenuto la medaglia d’argento, dimostrando che le macchine non si limitano più a calcolare numeri, ma stanno cominciando a padroneggiare l’arte del ragionamento logico.
Questa svolta non è un miracolo isolato dell’ingegneria; è il risultato di un’evoluzione decennale nel modo in cui verifichiamo la verità attraverso il codice. Nel suo nuovo libro, The Proof in the Code, il giornalista Kevin Hartnett esplora l’improbabile viaggio di Lean, uno strumento software che si è trasformato da assistente di codifica di nicchia nella spina dorsale della moderna verifica matematica e dello sviluppo dell’intelligenza artificiale.
Il ponte tra codice e logica
La storia inizia con Leo de Moura, un ex ingegnere di Microsoft Research che ha lanciato Lean nel 2013. Originariamente progettato come strumento per verificare la presenza di errori nel codice del software, il vero potenziale di Lean risiede nella sua somiglianza strutturale con la matematica.
Come sottolinea Hartnett, le due discipline condividono un DNA fondamentale:
– Sintassi: Entrambi richiedono istruzioni precise e passo dopo passo.
– Logica: un singolo errore in una riga di codice è funzionalmente identico a un “gap” in una dimostrazione matematica.
– Esecuzione: Proprio come un programma viene eseguito solo se la logica è corretta, un teorema matematico è valido solo se la sua dimostrazione è ineccepibile.
Questa consapevolezza ha innescato un movimento. Sebbene Lean non potesse “inventare” nuova matematica da sola, ha agito come un dimostratore di teoremi interattivo. Potrebbe essere necessaria una prova scritta da esseri umani, che potrebbe estendersi su centinaia di pagine e richiedere mesi per la revisione tra pari, e verificarne l’assoluta correttezza in un istante.
La lotta per un “linguaggio matematico”
Il passaggio dalla matematica tradizionale alla dimostrazione digitale non è stato fluido. Per anni, i matematici hanno dovuto affrontare uno scoraggiante problema “dell’uovo e della gallina”: per rendere utile il Lean, avevano bisogno di vaste librerie di definizioni matematiche codificate; ma per costruire quelle biblioteche avevano bisogno che i matematici usassero il programma.
L’attrito era spesso assurdamente granulare. Hartnett descrive come il professor Kevin Buzzard dell’Imperial College di Londra, mentre insegnava agli studenti universitari, si trovò bloccato perché Lean gli chiese di dimostrare che 2 non è uguale a 1. Per un essere umano, questa è una verità ovvia; per un sistema logico formale, è un fatto fondamentale che deve essere definito esplicitamente prima che possa verificarsi qualsiasi ulteriore ragionamento.
Superare questi ostacoli ha richiesto sforzi massicci e collaborativi:
* Digitalizzazione massiccia: nel 2018, i matematici hanno trascorso mesi a tradurre concetti complessi come gli “spazi perfettoidi” in migliaia di righe di codice.
* Creazione di comunità: un piccolo e dedicato gruppo di ricercatori ha lavorato per rendere il software facile da usare, trasformandolo da un goffo strumento accademico a una piattaforma solida.
* Amplificazione: entro il 2025, l’ecosistema era esploso, con decine di migliaia di utenti nel mondo accademico e nel settore tecnologico che contribuivano alle biblioteche Lean.
Perché è importante: la ricerca di una “macchina della verità”
La convergenza tra matematica e intelligenza artificiale è l’obiettivo finale di questo movimento. Per gli ingegneri del software come de Moura, il premio era una “macchina della verità” in grado di garantire che software come Microsoft Word fossero completamente privi di bug. Per i matematici, è un modo per garantire che anche le scoperte più complesse e astratte siano irreprensibili.
Per i ricercatori nel campo dell’intelligenza artificiale, il Lean rappresenta il campo di addestramento definitivo. Fornendo un’enorme libreria verificata di verità matematiche, Lean consente a modelli come AlphaProof di apprendere un ragionamento rigoroso anziché limitarsi al riconoscimento di schemi. Ciò è fondamentale per risolvere il problema delle “allucinazioni” nell’intelligenza artificiale: la tendenza dei modelli a dichiarare con sicurezza informazioni false. Se un’intelligenza artificiale potesse essere addestrata a seguire le rigide e inflessibili leggi della logica matematica, alla fine potrebbe applicare lo stesso rigore al ragionamento del mondo reale.
“Sia [la matematica che la codifica] sono scritti nella sintassi esatta come una serie di passaggi logici, ognuno dei quali porta al successivo.”
Conclusione
The Proof in the Code racconta come uno strumento specializzato per il debug del software sia diventato la base per una nuova era di certezza matematica e intelligenza artificiale. Evidenzia un profondo cambiamento nella scienza: il movimento verso un futuro in cui l’intuizione umana e la verifica digitale lavorano in tandem per definire ciò che è vero.
