Nel vasto panorama degli scienziati, i matematici sono sempre stati delle creature atipiche. Se è facile immaginare il fisico a lavoro con laser e acceleratori di particelle, il chimico in camice e occhiali tra alambicchi e provette, e il biologo chino su un microscopio a esaminare vetrini, è molto più difficile assegnare al matematico i suoi strumenti di lavoro, che spesso si riducono a carta e penna, o a grandi lavagne, rigorosamente a gesso.

In effetti, per secoli, il lavoro del matematico è stato svolto per lo più nelle teste e nei discorsi dei grandi pensatori, su fogli di corrispondenza, quaderni, blocchi notes o lavagne nelle aule delle università e dei centri di ricerca. Questo perché il lavoro di ricerca del matematico è composto per lo più, non da esperimenti, osservazioni o misurazioni, ma da dimostrazioni, che altro non sono che puro esercizio di pensiero, o almeno, così ce le insegnano a scuola.

In realtà, cosa sia esattamente una dimostrazione, cosa sia dimostrabile e quali siano gli strumenti per farlo, sono concetti che nel tempo hanno subito varie metamorfosi e continuano ad evolversi. In questo articolo faremo un rapido excursus di come è cambiato il lavoro del matematico nei secoli, per poi soffermarci su quello che sta succedendo oggi.

Sofisticatissimi software, dal promettente nome di “dimostratori di teoremi” (theorem prover), da qualche anno hanno fatto la loro comparsa sulle scene matematiche. Come sempre, qualcuno ha già pronosticato il loro sopravvento sulla romantica immagine del matematico assorto nei suoi calcoli. In realtà, per le tecnologie attuali, sembra difficile che l’esercizio dimostrativo nella sua interezza, e soprattutto nella sua parte creativa, possa venire completamente automatizzato. È però interessante ripercorrere il percorso che ci ha portato fino alle innovazioni attuali, per vedere in che modo i dimostratori automatici si stiano sempre più affermando come assistenti irrinunciabili dei matematici moderni.

Una breve storia della dimostrazione

La storia della logica moderna si fa risalire ad Aristotele, il padre del sistema deduttivo e del sillogismo (“Tutti gli uomini sono mortali, Socrate è un uomo, dunque Socrate è mortale”). Aristotele viene infatti considerato il primo ad aver formalizzato la definizione di assioma e di concetto primitivo, cioè di quelle verità, prive di ulteriore definizione, da cui il sistema deduttivo fa discendere tutte le altre proposizioni considerate vere. Molti di noi ricorderanno i concetti primitivi di punto, retta e superficie che ci sono stati presentati in geometria euclidea insieme ai cinque assiomi di Euclide. Su questi si costruisce ogni altro teorema della geometria, come quello di Pitagora o di Talete, mediante implicazioni logiche.

Possiamo immaginare il processo come la costruzione di un edificio, in cui gli assiomi e i concetti primitivi costituiscono le fondamenta, e ogni teorema rappresenta un mattoncino che eleva il muro. L’atto di aggiungere il mattoncino è appunto la dimostrazione, che permette di verificare che il risultato segua logicamente dagli assiomi, o, nella metafora, che il mattone sia compatibile con le fondamenta.

Per lungo tempo la logica aristotelica è stata alla base del sapere matematico e scientifico. In realtà, questa non è mai stata scevra da paradossi, ma bisogna aspettare la fine del XIX secolo perché venga messa in discussione. È in questo secolo, grazie al lavoro di grandi matematici come Riemann e Hilbert, che si introduce un nuovo paradigma: anziché pensare alla matematica come a un unico edificio costruito su assiomi fissi e immutabili, si inizia a considerare sistemi assiomatici diversi, o, in altre parole, a costruire più edifici in parallelo, partendo da fondamenta diverse.

Sono gli anni in cui si inizia a parlare di geometrie non euclidee, in cui data una retta e un punto esterno ad essa, possono passare per quel punto una retta parallela, infinite o nessuna, a seconda del sistema assiomatico di riferimento. In questo periodo, sembra che tutto il sapere matematico possa essere unificato e esteso ad libitum. È in quest’ottica che tra il 1910 e il 1913 Russell e Whitehead pubblicano i loro Principia Mathematica, opera mastodontica, con l’ambizioso scopo di riportare tutta la matematica a un unico sistema assiomatico coerente, cioè privo di contraddizioni.

Il 1931 è l’anno del duro risveglio: Kurt Gödel pubblica i suoi teoremi di incompletezza con cui mostra che, non importa come si scelgano gli assiomi, in ogni teoria ci saranno proposizioni vere ma indimostrabili. In altre parole, non importa come si scelgono le fondamenta, le mura dell’edificio matematico avranno sempre dei buchi, dei mattoncini mancanti che non possono essere collocati.

Con Gödel tramonta la speranza di una teoria basata su un unico sistema assiomatico. Nella pratica però, l’attività dei matematici è continuata imperterrita a porre, mattoncino sopra mattoncino, nuovi risultati nel grande edificio matematico. Il sistema assiomatico in cui oggi lavorano la maggior parte dei matematici si chiama ZFC (Zermelo-Fraenkel), ed è a questo quadro logico che si può riportare la maggior parte della matematica oggi studiata nelle università.

Un lavoro difficile

Ma cosa vuol dire dimostrare un teorema? Il processo attraverso cui un nuovo risultato è accettato all’interno dello scibile matematico è comune anche a molte altre scienze, ed è quello della peer-review. Un matematico che crede di aver dimostrato correttamente un nuovo risultato scrive la dimostrazione in un articolo che viene poi esaminato da un comitato di altri matematici. Questi controllano la correttezza della dimostrazione e danno il via libera alla pubblicazione del risultato, che diventa quindi parte della letteratura scientifica.

A differenza di altre scienze, in matematica la verità di un risultato dev’essere provata logicamente, e non sperimentalmente. Per fare un esempio: perché l’efficacia di un farmaco venga accettata dalla comunità scientifica, questo dev’essere testato e i suoi effetti sui pazienti devono essere opportunamente misurati. Se le misurazioni vengono considerate statisticamente sufficienti a confermare l’efficacia, il farmaco viene accettato come efficace. In matematica, per dire che tutti i numeri primi tranne il 2 sono dispari, non basta mostrare cento, centomila, o cento milioni di numeri primi dispari. Bisogna dimostrare logicamente che non può esistere un numero primo pari oltre il 2. Per questo diventa di fondamentale importanza che i revisori siano in grado di comprendere e verificare ogni passaggio di una dimostrazione, ed è proprio qui che si nascondono le insidie.

Ci sono stati casi di teoremi molto noti, come l’ultimo teorema di Fermat e il teorema dei quattro colori, in cui, dopo secoli dalla loro enunciazione, è stato affermato di aver trovato una dimostrazione, rivelatasi però sbagliata. Nel caso del teorema dei quattro colori, dimostrato indipendentemente da Kempe e Tait, rispettivamente nel 1879 e nel 1880, ci sono voluti undici anni per trovare l’errore. Nel caso dell’ultimo teorema di Fermat, la dimostrazione presentata da Andrew Wiles nel 1993, dopo sei anni di lavoro, verrà rifiutata sulla base di un errore che necessiterà di altri quindici mesi di lavoro per essere corretto da Wiles stesso.

Ma c’è di più, a volte il problema non è trovare gli errori, ma comprendere la dimostrazione stessa. Nel 2003 il matematico russo Grigori Perelman annunciò di aver dimostrato la congettura di Poincaré, enunciata nel 1904 e per cui il Clay Institute of Mathematics aveva messo in palio un milione di dollari. Ci vollero però ben tre anni di dibattito per convincere la comunità scientifica ad accettare come vera la dimostrazione di Perelman, che, alla fine, nel 2006, rinunciò al premio in denaro.

Ancora più recentemente, nel 2012, Shinici Mochizuki, un matematico giapponese, ha pubblicato oltre 500 pagine in cui affermava di aver dimostrato diverse importanti congetture di teoria dei numeri e geometria aritmetica. Nel 2018 alcune di queste dimostrazioni sono state contestate da altri matematici, a cui Mochizuki ha risposto dicendo che non avevano compreso correttamente la sua dimostrazione. E in effetti, la comunità scientifica tuttora fatica a comprendere le pubblicazioni del giapponese, che di fatto non vengono accettate come vere, non essendo state verificate. Insomma, sembra che la matematica sia arrivata ad un punto in cui gli uomini non bastano per verificare cosa è vero. Ed è qui che entrano in gioco le macchine.

Arrivano le macchine

I primi dimostratori automatici risalgono agli anni ’50-’60, quando, con la diffusione dei primi computer, si iniziò a pensare alla possibilità di automatizzare il processo dimostrativo. I primi tentativi portarono a programmi in grado di ridimostrare autonomamente risultati già noti, come i teoremi di geometria euclidea o alcuni dei teoremi dei Principia di Russell e Whitehead.

Questi programmi hanno una duplice natura, informatica e matematica, e vengono percepiti in maniera molto diversa dalle due comunità. Per la comunità degli informatici, più incline all’automatizzazione, i dimostratori automatici sono stati visti sin dai loro inizi come preziosi strumenti per la verifica della correttezza dei programmi. Questo campo dell’informatica, che si chiama appunto “verifica”, utilizza dimostratori automatici per dare delle garanzie sul fatto che un programma rispetti le specifiche per cui è stato scritto, cioè, faccia effettivamente quello che vuole il suo programmatore. Questo è particolarmente importante in campi come la sicurezza e la finanza in cui è necessario garantire che un programma non esegua comandi pericolosi che, per esempio, potrebbero rendere una password o un conto bancario accessibili a un hacker.

I matematici si sono approcciati all’automatizzazione del ragionamento con molto più scetticismo. Nel 1977 il teorema dei quattro colori, lo stesso le cui dimostrazioni date nel 1879 e nel 1880 erano risultate sbagliate, è stato dimostrato utilizzando un computer. Lo stesso è successo nel 1998 per la congettura di Keplero e nel 2016 per il problema booleano delle terne pitagoriche. In tutti e tre i casi però le dimostrazioni sono incredibilmente lunghe e complicate e la loro correttezza non può essere verificata facilmente dai matematici in carne ed ossa. Come conseguenza, la loro validità è spesso controversa.

Recentemente le cose hanno preso una nuova piega. Se è vero che una dimostrazione completamente costruita da un computer rischia di diventare incomprensibile, sembra molto più promettente l’approccio, simile a quello usato in informatica, di usare programmi ad hoc per verificare la correttezza di un ragionamento.

Nel 2013 è nato Lean, un progetto open-source che tramite un programma e un linguaggio di programmazione dedicato permette di verificare la correttezza di una dimostrazione matematica. Utilizzando Lean è possibile “trascrivere” una dimostrazione in modo che il programma sia in grado di verificare tutti i passaggi logici siano corretti. Ma c’è di più: ogni volta che un nuovo teorema viene verificato tramite Lean, esso entra a far parte di mathlib, una libreria che Lean potrà utilizzare nelle sue future verifiche. Insomma, Lean si comporta come un matematico in grado di ricordare tutte le dimostrazioni che ha letto, e perciò di verificare se una nuova dimostrazione è corretta o no in base ai risultati già visti.

La rapida crescita di mathlib ha segnato uno spostamento nella mentalità della comunità matematica, spinto soprattutto dai più giovani, ma non solo. La necessità di un controllo più oggettivo e rigoroso era da tempo diffusa nella comunità. Peter Scholze, che nel 2018 ha ricevuto il più prestigioso premio della matematica, la medaglia Fields, ha usato proprio Lean per verificare le sue dimostrazioni. Insieme a Lean si è assistito a una fioritura nel campo degli assistenti automatici alle dimostrazioni, come una rapida ricerca su Wikipedia può testimoniare.

Ma c’è chi guarda ancora oltre: uno studio del 20201 ha mostrato che delle reti neurali debitamente addestrate sono state in grado di generare e provare nuovi risultati. In altre parole, un algoritmo è riuscito a enunciare nuovi teoremi e a dimostrarli correttamente. Questo nuovo sviluppo sembra però ancora piuttosto lontano dal trovare applicazioni pratiche: inventare un nuovo problema è relativamente facile, risolverlo lo è meno, ma la vera difficoltà della ricerca matematica sta nel risolvere i problemi interessanti, per cui ancora l’automatizzazione non sembra essere alla nostra portata.

In definitiva, nelle stanze dei matematici si sta assistendo a una piccola rivoluzione, in cui parte del lavoro si sta spostando dalle menti e dai fogli di carta, ai circuiti dei computer. Sorprendentemente, non si tratta della parte fatta di lunghi e noiosi calcoli, più o meno complessi, in cui i computer ci avevano superato già da tempo, ma del lavoro logico e razionale, finora prerogativa dei cervelli umani. Un futuro in cui i computer soppiantano i matematici sembra ancora lontano, ma uno in cui il matematico lavora affiancato da un fedele compagno con il cervello al silicio è già realtà. Parafrasando Dick, non sappiamo se gli androidi sognano di essere matematici, ma, come Lean, si stanno rivelando discreti studenti.

Note

1 Urban, J., & Jakubův, J. (2020). First neural conjecturing datasets and experiments. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13 (pp. 315-323). Springer International Publishing.