Un teorico dei numeri ha paura che tutta la matematica in circolazione sia sbagliata

C'è una contaminazione informatica in corso nel mondo della matematica pura. Alcune dei pesi massimi del campo, per quanto rinomati per la loro autosufficienza di pensiero, cominciano ad affidarsi ai software per capire e verificare le loro dimostrazioni.

Kevin Buzzard, un teorico dei numeri e professore di matematica pura all'Imperial College di Londra, crede che sia ora di creare una nuova area della matematica, dedicata alla computerizzazione delle dimostrazioni. Alcune delle più importanti oggi sono diventate talmente complesse che praticamente nessun essere umano sulla Terra può capirne i dettagli, figuriamoci dimostrarle. Teme che molte delle dimostrazioni considerate vere, siano in realtà false. C'è bisogno di aiuto.

Che cos'è una dimostrazione? È un processo di deduzione della validità di un assunto matematico. Le dimostrazioni si sommano poi tra loro e le persone imparano così la matematica, che viene poi applicata in altri campi.

Per creare una dimostrazione, si inizia da una definizione. Per esempio, definiamo un set di numeri come gli interi, ovvero tutti i numeri interi che vanno da meno infinito a più infinito. Scrivi questo insieme come: …., -2, -1, 0, 1, 2, … Poi, formuli un teorema; per esempio, che non esiste un numero intero più grande di tutti. La prova consiste nel ragionamento logico che dimostra il teorema come vero o falso—in questo caso, vero. I passaggi logici nella dimostrazione si appoggiano su altre verità precedenti, che sono già state accettate e dimostrate. Per esempio, che il numero 1 è più piccolo del numero 2.

Qualsiasi nuova dimostrazione ottenuta da matematici professionisti tende ad appoggiarsi su un intero bacino di risultati precedenti che sono già stati pubblicati e compresi. Ma Buzzard dice che, in molti casi, le dimostrazioni precedenti su cui se ne costruiscono di nuove non sono affatto comprese chiaramente. Per esempio, ci sono paper di rilievo che citano apertamente lavori teorici ancora non pubblicati. Questo preoccupa molto Buzzard.

"Mi sorge la paura che tutta la matematica pubblicata sia in realtà sbagliata, perché i matematici non controllano i dettagli, e hanno commesso altri sbagli prima d'ora," ha detto Buzzard a Motherboard mentre si trovava alla 10ma conferenza di Interactive Theorem Proving a Portland, in Oregon, dove ha tenuto il discorso d'apertura.

"Credo che ci sia una possibilità superiore a zero che alcuni dei nostri più grandi castelli siano fatti di sabbia," ha scritto Buzzard in una delle slide della sua presentazione. "Ma penso anche che sia piccola."

La nuova matematica dovrebbe essere comprovata da testa a piedi. Ogni passaggio deve essere controllato, o almeno il ragionamento che segue. D'altro canto, ci sono esperti e veterani della comunità di matematici che forniscono una guida affidabile a cosa è vero e cosa no. Se una di queste figure eminenti cita un paper e lo usa per il suo lavoro, allora quel paper probabilmente non ha bisogno di essere controllato, pensiamo tutti.

Il punto del discorso di Buzzard è che la matematica moderna è diventata troppo dipendente dalla parola degli "anziani" perché i risultati sono diventati troppo complessi. Una nuova dimostrazione può richiedere la citazione di anche 20 altri paper, e uno solo di questi 20 ha magari 1.000 pagine e rotte di ragionamenti densissimi. Se un matematico rispettato cita il paper da 1.000 pagine e parte in qualche altro modo dai suoi presupposti, allora molti altri matematici possono semplicemente assumere che il paper da 1.000 pagine (e la nuova dimostrazione) siano veri e non si prenderà la briga di controllare. Ma la matematica deve essere universalmente dimostrabile, non contingente a una manciata di esperti.

Tutto questo rende più fragile la comprensione della verità. Una dimostrazione dell'ultimo teorema di Fermat, proposta nel 1637 e una volta considerata dal Guinness dei Primati come "il teorema matematico più complesso," è stata pubblicata negli anni Novanta. Buzzard sostiene che nessuno in realtà la capisce davvero per intero, o sa se è vera o no.

"Penso che nessun essere umano, vivo o morto, sappia tutti i dettagli della dimostrazione dell'ultimo teorema di Fermat. Ma la comunità lo accetta lo stesso," ha scritto Buzzard nella sua presentazione. Questo perché "gli anziani hanno decretato così."

Un paio di anni fa, Buzzard è incappato in conferenze tenute dai matematici Thomas Hales e Vladimir Voevodsky, che lo hanno introdotto ai software di verifica, un campo in netta crescita. Con un software del genere, le dimostrazioni possono essere verificate sistematicamente da un computer, rendendo la verità più democraticamente accessibile.

Quando Buzzard ha iniziato a usare un programma di verifica chiamato Lean, é rimasto stregato. Non solo il software gli permetteva di verificare le dimostrazioni oltre ogni ragionevole dubbio. Il software lo aiutava anche a pensare alla matematica in un modo molto chiaro e lucido.

"Ho capito che i computer accettano solo input in una forma molto precisa, che è il mio modo preferito di pensare alla matematica," ha detto Buzzard. "Mi sono innamorato, perché è come se avessi trovato un'anima gemella. Qualcosa che pensa la matematica come faccio io."

Per verificare la sua dimostrazione, un utente di Lean deve formalizzarla, o convertirla dalla lingua umana ai simboli che il linguaggio di programmazione di Lean usa. L'utente deve anche formalizzare qualsiasi definizione e dimostrazione sussidiaria su cui si basa il suo nuovo lavoro. Per quanto questo processo di conversione sia laborioso, Lean sembra in grado di gestire qualsiasi pezzo di matematica che Buzzard gli propina.

Lean ha attirato l'interesse di molti matematici, in particolare di chi si occupa di insegnamento. Jeremy Avigad è un progessore della Carnegie Mellon, specializzato in teoria della dimostrazione. Sia Avigad che Buzzard hanno iniziato a usare Lean nelle loro lezioni introduttive alla materia. Il software controlla la validità di ogni riga di una dimostrazione e fornisce un feedback, che è molto utile per gli studenti.

Per quanto Avigad sia felice che la comunità sia interessata a Lean, sostiene che la tecnologia abbia bisogno ancora di migliorare. Questo genere di programmi portano via molto tempo. "Il settore esiste da decenni ed è sempre meglio, ma non siamo ancora a un punto di svolta," ha detto.

Se questi ostacoli saranno superati, Buzzard ritiene che il software potrebbe avere conseguenze che vanno oltre le dimostrazioni. Prendiamo per esempio il problema della ricerca. Ogni anno vengono pubblicate tonnellate di nuovi risultati e poterli navigare è estremamente importante.

Hales e Buzzard hanno ipotizzato che se l'abstract di ogni nuovo paper fosse inserito dentro Lean, un matematico potrebbe sondare il database in cerca di un oggetto matematico preciso e trovare tutto ciò che è già stato scritto a riguardo. In un certo senso, le menti imperscrutabili dei veterani potrebbero essere riversate e rese disponibili per tutti

Gli informatici potrebbero usare questo database per allenare le intelligenze artificiali. Dato che i risultati sarebbero definiti secondo il linguaggio preciso di Lean, sarebbe molto più semplice per un programma imparare così che non decifrando frasi in inglese.

Alla fine, qualcuno potrebbe creare un verificatore di teoremi automatizzato generale, un programma che possa creare le proprie dimostrazioni, fare matematica da solo. La tecnologia che questi programmi usano è già la stessa di Lean e la diffusione di quest'ultimo potrebbe rivelarsi un passaggio formativo importante per l'automazione generale della matematica.

Michael Harris, professore di matematica alla Columbia e collega di Buzzard, è preoccupato però informatici e aziende tech non condividano le stesse motivazioni dei matematici. I primi, per esempio, vogliono usare la tecnologia di Lean per verificare che un software sia privo di bug. Le aziende, invece, vogliono trarne profitto. I matematici come Buzzard vogliono solo farci matematica.

"Una cosa che posso dire è che se persone davvero intelligenti come Thomas Hales e buzzard continueranno a pensare in questo modo, allora salterà fuori qualcosa di interessante; magari non sarà un'IA, ma nuove branche di studio della matematica o persino un nuovo modo di pensare," ha detto Harris.