Anche la matematica è in crisi! Possibile?

Larga parte della matematica che si produce è fuori controllo. Senza dimostrazione!

Il controllo delle dimostrazioni.

Immaginare una matematica in crisi non è proprio una banalità. È come se conoscenze e sapere perdessero qualcosa, in particolare solidità e luminosità. Eppure la matematica nel corso della storia ha avuto non uno ma più momenti di crisi. Ha vissuto certamente, come si racconta, un momento di crisi ai tempi di Pitagora con la scoperta dell’irrazionale e poi, ancora, a cavallo tra il XIX e il XX secolo, con la profonda e nota crisi dei fondamenti. Di crisi si è parlato anche negli anni Sessanta e Settanta del secolo scorso con riferimento ad una sopraggiunta, pervasiva, indecidibilità di proposizioni matematiche con conseguente “perdita della certezza”. Quella attuale sarebbe una crisi della dimostrazione. Anzi, più che altro, una crisi del controllo delle dimostrazioni. Ne parla Marianne Freiberger in un articolo apparso su Plus magazine.

Nell’articolo l’autrice riporta i risultati di un seminario tenuto a Cambridge da Kevin Buzzard, professore di Matematica pura presso l’Imperial College, il quale si occupa da tempo della ‘verifica formale’ delle prove ed è il titolare di un progetto denominato LEAN che mira alla meccanizzazione delle procedure dimostrative formalizzando la matematica che è effettivamente usata dai matematici.

Nel corso del seminario Buzzard avrebbe detto che il campo delle dimostrazioni si presenta davvero disastrato. Ci sono dimostrazioni con buchi o salti logici, dimostrazioni con errori e dimostrazioni che sono capite solo da una o due persone nel mondo intero e questo è il caso più diffuso. La situazione descritta presenta elementi di disagio non nuovi, già evidenziati da qualche tempo. Il disagio però è crescente. Dal settore della ricerca pura sta progressivamente investendo anche chi è impegnato nel rinnovamento dell’insegnamento e chi si occupa della divulgazione dei nuovi risultati. È una situazione che ha finito per generare più di un dubbio sulla verità di quanto pubblicato su riviste anche di prestigio. Sono dubbi che indeboliscono la fiducia verso l’accademia. Dubbi che accreditano l’esistenza, in analogia a quanto avviene in genere nella strategia della comunicazione, di esperti responsabili del reperimento del consenso.

Ecco: le cose sono un po’ fuori controllo, è la sintetica affermazione di Buzzard.                                                                                                             

È vero, Pascal diceva: quanto è difficile avere le prove sempre pronte! Oggi pare che la difficoltà si superi ricorrendo anche a stratagemmi, talvolta intenzionalmente “diretti ad ingannare”! Non è raro, infatti, che in uno specifico lavoro di ricerca gli autori facciano riferimento ad altre loro pubblicazioni inedite. In tal modo poggiano le conclusioni su risultati dati per acclarati ma non ancora pubblicati. Cosa che spesso poi non avviene. Si dà il via in tal modo ad una catena di moltiplicazione degli errori, costruita da altre persone che lavorando fondano fiduciosamente il proprio impegno di ricerca su quei risultati non controllati. Buzzard ha riportato vari esempi di lavori a stampa che hanno ricevuto anche dei premi internazionali, ma basati su dimostrazioni con evidenti buchi logici e dunque non pienamente ‘sane’. È questa una situazione che preoccupa e che non si può lasciare inaffrontata, perché è perdita della fiducia, che è l’intimo umano legame della comunità dei matematici. Essa rischia cioè di modificare le regole  umane e sociali che hanno sempre caratterizzato l’ambiente professionalmente sano della matematica, inficiandone i valori di correttezza e verità.

Il dilemma di Ulam e la complessità delle dimostrazioni

È ovvio, errori nelle dimostrazioni ci sono sempre stati. Ognuno commette errori e talvolta questi errori sfuggono anche agli esperti referees che decidono se pubblicare un documento. La storia è ricca di episodi di errori nelle dimostrazioni che sono stati poi riconosciuti e corretti. Il fatto è che la produzione odierna è molto consistente. Quanto? Ad affrontare il calcolo pensò già Stanislaw Ulam, che ne parla in Adventures of a Mathematician del 1976. Consegnò così alla storia un problema che Philip J. Davis e Reuben Hersh in The Mathematical Experience (1981) battezzarono come dilemma di Ulam. Nella marea di teoremi e lemmi annualmente prodotti la scoperta di un errore e la sua correzione possono dunque richiedere tempo e non raggiungere tutti i lettori, figurando a volte in un breve erratum. Al numero di pubblicazioni, però, si aggiunge quello che forse è il problema più grosso. Le dimostrazioni sono per lo più divenute tanto lunghe e complesse da richiedere sforzi enormi per essere comprese e dominate. I campi di ricerca sono poi così specifici e differenziati che solo poche persone possono essere interessate ad un particolare risultato e essere in grado di valutarne la correttezza.

Ci sono dimostrazioni che solo poche persone al mondo capiscono.

Un esempio famoso è la classificazione dei gruppi semplici finiti. Un trionfo della matematica del XX secolo che, come suggerisce il nome, consiste nella classificazione in un certo numero di ‘famiglie’ di una quantità  infinita di oggetti matematici. La dimostrazione che la classificazione era corretta e completa, nella sua prima versione, “apparve nel 1983 e da sola riempiva più di 10.000 pagine, distribuite in 500 articoli di riviste, da oltre 100 autori diversi”. In effetti un teorema policefalo, non dominato da una sola mente. Data questa enorme complessità, i principali autori si sono impegnati da tempo nella creazione di una versione “più semplice” di seconda generazione, da pubblicare in dodici volumi, dei quali fino ad oggi ne sono apparsi solo sette. Probabilmente la prova completa è stata capita solo da pochissime persone e “nessuna di queste sta diventando più giovane”. I matematici in genere concordano sul fatto che la classificazione dei gruppi semplici finiti sia effettivamente completa e che qualcuno in grado di seguire l’enorme quantità di letteratura disponibile dovrebbe essere in grado, prima o poi, di metterne insieme la dimostrazione. Ma quante persone hanno il tempo (e il cervello) per farlo?

La minaccia per la matematica e la perdita del significato

C’è chi crede che questo tipo di problemi minacci la matematica pura a tal punto da farla scivolare in una crisi d’identità. Ma cosa si deve fare? La matematica è un soggetto creativo, non procedurale. E i matematici sono essere umani ai quali piace confrontarsi e lavorare in gruppo e che non amano essere impantanati dai dettagli. Chiedere loro di attenersi sempre al rigore delle procedure è come chiedere loro di lavorare come macchine.   

La soluzione?

Forse, suggerisce Buzzard, è proprio nel rapporto con le macchine. “Occorrerà non chiedere ai matematici di lavorare come macchine, ma chiedere loro di usare macchine”. Scienziati informatici e matematici formano due tribù diverse, imparentate sì, ma con differenze essenziali. “Gli informatici correggono i bug, mentre i matematici li ignorano”, afferma Buzzard. Gli informatici, alcuni dei quali spesso si aggirano tra i matematici, hanno sviluppato software di dimostrazione di teoremi come LEAN non per sostituire il matematico-uomo, ma per aiutarlo a verificare che le prove siano valide. Uno scienziato informatico, dice Buzzard, potrebbe sostenere che un risultato non è dimostrato fino a quando non è stato formalmente controllato dal software di dimostrazione del teorema. Ciò significa che molti risultati monumentali in matematica, tra cui l’ultimo teorema di Fermat o il già citato ‘teorema enorme’ della classificazione dei gruppi finiti semplici, nella mente di uno scienziato informatico necessitano di essere controllati con maggiore attenzione. Buzzard affronta a questo punto un’altra questione che circonda l’uso dei computer in matematica. La paura che la vera comprensione potrebbe essere persa.

Ad una riacquistata certezza formale dei risultati si accompagnerebbe così una perdita del significato.

“Se i computer fanno il nostro lavoro per noi, e se lo fanno in un modo che la nostra scarsa capacità di elaborazione dei dati non ci consente di seguire, allora non possiamo pretendere di comprendere i risultati che emergono”.

È quanto si obietta a Buzzard, il quale ribatte affermando che “piuttosto che rendere le prove inaccessibili agli umani, vorrebbe renderle accessibili ai programmi per computer che possono controllarle con grande affidabilità”.     Un’affermazione che non è priva di concretezza. Ed è la sintesi dell’esposizione che Buzzard fa del suo programma di lavoro, la cui meta è il raggiungimento di una nuova tappa del cammino del computer come dimostratore di teoremi. Un cammino iniziato più decenni fa.

Nel 1959 il computer dimostrò che gli angoli alla base di un triangolo isoscele sono uguali.

Il ragionamento utilizzato era ridotto all’osso. Eminentemente sintetico, non seguiva la sistemazione della geometria di Euclide – lo racconta, tra gli altri, Jeremy Bernstein in Uomini e macchine intelligenti, Adelphi 1990. Un’altra tappa del percorso è la dimostrazione mista: una parte ragionata, un’altra meccanica. Una dimostrazione frutto del connubio di mente e macchina. Accadde nel 1976 quando Kenneth Appel e Wolfgang Haken dettero risposta ad un problema che era noto da più di un centinaio di anni come “congettura dei quattro colori”. In effetti avevano “spezzettato il problema in migliaia di casi che il computer aveva elaborato uno dopo l’altro”. Più che l’annunciata soluzione, a fare notizia fu il metodo dimostrativo. Era una dimostrazione?

Perché credere ad un computer?

“Se accettiamo come teorema – fu il parere di Stephen Tymoczko – il teorema dei quattro colori, siamo costretti a modificare il significato di ‘teorema’ o,  ciò che più conta, a modificare il significato del concetto sottinteso di ‘dimostrazione’ ”. La risposta di Wolfgang Haken non fu meno interessante: “Chiunque, in qualunque punto della dimostrazione, può supplire i dettagli e verificarli. Il fatto che il calcolatore  sia in grado di elaborare in alcune ore più dettagli di quanti un essere umano possa mai sperare di esaminare nel corso di una vita non modifica il concetto fondamentale di dimostrazione matematica. Quel che è cambiato non è la teoria, ma la pratica della matematica”. 

Interrogativi finali.

Il computer si è insinuato tra umano e non umano. Vi gioca un ruolo analogo a quello dell’insieme dei numeri complessi per Eulero: amphibium inter ens et non ens. È prolungamento della mente umana e nuovo ponte per unire ciò che è opposto, teoria/pratica, naturale/artificiale. Nel programma di Buzzard, che non è solo di ricerca ma è pure didattico, i matematici e gli studenti, aspiranti matematici, sono i frequentatori di una biblioteca della quale il computer è il titolare. Il responsabile della conservazione e della catalogazione di testi dei quali è anche garante della correttezza e editore. La matematica sta davvero traslocando nella biblioteca dei programmi formali controllati dalla mente di silicio? Non risiede più solamente nella natura come voleva Platone, né nella mente umana come voleva Aristotele. Tra le sedi c’è anche il computer che la sta ereditando? Difficile allora continuare a riferirsi alla bella definizione di Richard Courant e Herbert Robbins:

“Come espressione della mente umana la matematica è volontà attiva, ragione contemplativa, desiderio di perfezione estetica”!

Sarebbe già negata! Che cos’è allora la matematica?

ALTRI RIFERIMENTI NEL SITO:

• I problemi ancora aperti
• I grandi momenti della matematica