Come possiamo essere sicuri che una dimostrazione matematica sia davvero corretta? E che cosa succede quando a produrre dimostrazioni – o codice – è un’intelligenza artificiale? In questo articolo, Matteo Acclavio e Fabrizio Montesi ci raccontano cosa sono i proof assistants e perché stanno cambiando il modo di fare matematica e informatica.

La matematica può essere vista come il più grande passatempo mai inventato dagli esseri umani: si fissano le regole del gioco (chiamate assiomi) e si discute con amici di ciò che ne consegue. Se una conclusione è inevitabile a partire dalle regole scelte, allora la si chiama teorema.

In certi casi, il gioco appare semplice. Per esempio, se si considerano i numeri naturali, allora per dimostrare che esistono infiniti numeri primi (cioè numeri più grandi di 1 e divisibili solo per se stessi e per 1), basta prendere un numero finito di numeri primi, moltiplicarli insieme e aggiungere 1 per ottenerne un numero che non è divisibile per nessuno dei numeri primi presi in considerazione, quindi o è un “nuovo” numero primo, o è divisibile per degli altri numeri primi, contraddicendo l’assunzione che l’insieme dei numeri primi di partenza li conteneva tutti.

Il motivo per cui questo ragionamento è relativamente breve e all’apparenza semplice è perché stiamo dando per scontato che siano chiari i significati (e le conseguenze) di concetti come “numero primo”, “insieme'”, “finito”, “divisibilità”, “somma” e “prodotto'”. In realtà, quanto sia veramente semplice capire il ragionamento precedente dipende dall’esperienza del lettore. Più il lettore è vicino ai concetti usati in una prova matematica, e più facilmente riuscirà a convincersi della sua correttezza (o mancanza di essa). Dal punto di vista dello scrittore della prova, c’è sempre una scelta linguistica importante da prendere su quanto dettagliata la prova debba essere e, in particolare, quanto vadano espansi i nomi tecnici.

Il problema aumenta immensamente di complessità quando si vogliono dimostrare teoremi che coinvolgono concetti più sofisticati, o quando si vuole essere sicuri che un teorema sia dimostrato in modo rigoroso e senza errori. Per esempio, nei Principia Mathematica, Alfred North Whitehead e Bertrand Russell impiegarono più di 300 pagine per dimostrare che 1+1=2 (uno più uno fa due, per essere chiari), partendo da un insieme di assiomi costruiti ad hoc per descrivere l’aritmetica. Per essere sicuri di non fare sbagli, questi assiomi utilizzano unicamente il ragionamento logico formale.

Questo è sicuramente un esempio estremo, ma illustra il punto: la matematica può essere incredibilmente complessa e difficile da verificare, anche per risultati semplici e per i matematici più esperti.

Sebbene discutere con i propri colleghi sia un modo efficace per verificare le dimostrazioni, non è sempre sufficiente. Soprattutto quando si tratta di teoremi complessi o risultati formulati all’interno di teorie sofisticate, avere un modo di essere sicuri che una dimostrazione sia corretta e priva di errori è fondamentale. Altrimenti, qualsiasi nuova teoria o applicazione costruita su quella dimostrazione rischia di essere sbagliata.

Gli assistenti di prova (o proof assistants) sono software nati per affrontare il problema di verificare le dimostrazioni matematiche in modo rigoroso e affidabile. Essi non solo forniscono un ambiente in cui si possono definire oggetti matematici e formulare teoremi (e le loro dimostrazioni) in un linguaggio condiviso, ma anche un sistema di verifica che assicura che ogni passaggio della dimostrazione sia corretto e che non ci siano errori logici in nessun passaggio.

I proof assistants sono una tecnologia sviluppata nel campo dell’informatica per la verifica dei modelli matematici usati per ragionare su software e computer in generale. In un certo senso, sono l’evoluzione (o una delle eredità) del programma di Hilbert sulla formalizzazione dell’intera matematica. Per decine di anni, l’utilizzo dei proof assistants è rimasto confinato alla ricerca specializzata in informatica o alle applicazioni industriali per la verifica di software critici, come sistemi operativi, protocolli di sicurezza e algoritmi di crittografia, dove un semplice bug in un programma potrebbe avere conseguenze disastrose.

Negli ultimi anni, però, la loro rilevanza sta rapidamente schizzando alle stelle per vari motivi. Primo tra questi, il fatto che le discipline scientifiche stanno diventando sempre più complesse e sofisticate, e i risultati che si vogliono dimostrare richiedono sempre più spesso un alto livello di specializzazione e competenza per essere compresi e verificati. Non è un caso che matematici come Terence Tao stiano parlando di una nuova era della matematica, dove persone da tutto il mondo possono contribuire con dimostrazioni che vengono ritenute affidabili (grazie alla verifica dei proof assistants) indipendentemente dalla loro reputazione o specializzazione.

In secondo luogo, il livello di confidenza che si vuole avere nei risultati scientifici è aumentato, soprattutto in campi come la fisica o l’informatica, dove i risultati dimostrati possono avere implicazioni pratiche significative. Per esempio, i requisiti di affidabilità di sistemi informatici che gestiscono dati privati, finanze, o vite umane stanno (giustamente) aumentando. In generale, l’ubiquità del software sta conducendo la società a ripensare quanto profondamente possiamo fidarci degli strumenti informatici che usiamo ogni giorno nelle nostre vite. La matematica sta emergendo come la possibile salvatrice che farà da ponte tra il codice delle macchine e la nostra comprensione di cosa questo codice veramente faccia.

Un altro fattore che sta contribuendo alla rilevanza dei proof assistants, specialmente negli ultimissimi anni, è il crescente interesse per l’intelligenza artificiale generativa, dove i proof assistants vengono usati come uno strumento chiave per affrontare la cosiddetta crisi dell’AI. Infatti, uno dei problemi principali dell’intelligenza artificiale generativa è la difficoltà di garantire che i risultati generati siano corretti e affidabili, soprattutto quando si tratta di output che coinvolge concetti complessi o risultati scientifici. Per esempio, se un modello di intelligenza artificiale generativa produce una dimostrazione matematica o del codice per un sistema informatico, come possiamo essere sicuri che quella dimostrazione o quel codice siano corretti e privi di errori? I proof assistants offrono una soluzione a questo problema, fornendo un sistema di verifica rigoroso che può essere utilizzato per verificare la correttezza di qualsiasi output generato da un modello di intelligenza artificiale.

Lean è uno dei proof assistants più popolari e utilizzati al giorno d’oggi, con una comunità di utenti in crescita e vaste librerie di definizioni, teoremi e dimostrazioni formali costruite collaborativamente dagli utenti di tutto il mondo (tutto in modo open source). Per esempio, la libreria Mathlib di Lean contiene più di 2 milioni di righe di codice, che includono teoremi e definizioni formali in molti campi della matematica, dalla teoria dei numeri alla topologia, dall’algebra alla geometria, e molto altro ancora. La libreria CSLib di Lean è invece una libreria il cui focus è su teorie e risultati di informatica, con particolare attenzione alle loro possibili applicazioni in teoria dei linguaggi di programmazione, verifica formale di software, sicurezza informatica, ed algoritmi in generale.

Progetti come Lean, Mathlib, e CSLib stanno causando uno tsunami di innovazione nel modo di lavorare per matematici ed informatici (e, in futuro, anche altre professioni): dal lavorare in piccoli gruppi fidati (con collegamenti sporadici tramite collaborazioni o conferenze internazionali) al lavorare in modo globale ed aperto, grazie al linguaggio universale offerto dai proof assistants. Questo tsunami ha coinvolto anche lo sviluppo di intelligenze artificiali. Infatti, i proof assistants non sono solo uno strumento per verificare l’output di una AI da parte dell’utente. Sono anche diventati un nuovo indispensabile insegnante nella famosa fase di addestramento delle AI, dove offrono continuamente feedback sulla validità delle dimostrazioni generate (giuste o sbagliate, e con descrizioni degli errori). Questo aumenta la qualità dell’output, rendendo le AI più utili ed affidabili.

Dove si collocano in questo nuovo mondo gli esperti di matematica e campi collegati, come l’informatica teorica? Cioè, come si sente chiedere ultimamente di consueto, l’intelligenza artificiale ci rimpiazzerà tutti? Quasi sicuramente no. Infatti, l’evoluzione che stiamo osservando è che umani esperti di modelli matematici servono sempre di più. In un mondo dove verificare prove generate da intelligenze artificiali è possibile su larga scala, salta fuori una domanda molto importante: quali teoremi dobbiamo chiedere alla AI di dimostrare? Rispondere a questa domanda richiede competenze, esperienza, e creatività. Quindi, per tutti gli esperti e studenti là fuori, c’è un messaggio molto chiaro: c’è un nuovo aiutante meccanico, un po’ come quando arrivarono i calcolatori; usatelo pure per fini pratici, pedagogici, o anche ricreativi (come dicevamo all’inizio, per molti la matematica è anche un divertimento). Non c’è niente di cui aver paura, anzi, il campo della matematica può sentirsi fiero di questa nuova influenza nel mondo.

Guarda la pagina  AILA x MaddMaths!