Medaglia Fields e ricercatore
rivoluzionario, è morto improvvisamente il 30 Settembre scorso a 51 anni a Princeton. E' stato il più
brillante cacciatore di errori nascosti. Ma spaziò in tutti i campi.
Era l’uomo che cercava gli
“errori nascosti”, un ricercatore geniale che si era concentrato anche sulla
possibilità della verifica automatica delle dimostrazioni. Il suo "Assioma
di univalenza" (un modello della teoria costruttiva dei tipi nella
categoria degli insiemi) è studiato nelle università di tutto il mondo. Lo ha
stroncato un ictus mentre si trovava a casa sua. E’ stato definito “uno tra i
più brillanti e rivoluzionari matematici della sua generazione”. Secondo Thomas
Hales, matematico all’Università di Pittsburgh, Voevodsky è stato “uno dei
giganti del nostro tempo", che trasformava ogni campo del quale si
interessava, “persino il significato del segno ‘uguale’ in matematica”. Voevodsky,
in sintesi, pensava che il cervello umano non è in grado di stare dietro alla
crescente complessità delle matematiche. L’unica soluzione sono i computer.
Così si impegnò in un ambizioso progetto per creare software così potenti e
convenienti che i matematici possano usare nel proprio lavoro.
"Le lezioni? Una perdita di
tempo"
Eppure Vladimir mostrò già a
scuola un carattere, e un ingegno, talmente forti da non promettere bene. Fu
cacciato da scuola e dall'ateneo tre volte, la prima perché litigò col suo
professore sul presunto comunismo dello scrittore Dostoevskji, su cui lui non
era d’accordo. Quindi fu allontanato dall’università di Mosca perché non
frequentava le lezioni, considerandole una perdita di tempo. Ricorda oggi il
matematico Tomás Gómez su ‘El País’: “Siamo soliti presumere che le verità
matematiche siano eterne. A differenza di altre discipline, in cui le teorie
considerate corrette possono essere rifiutate alla luce di nuovi risultati, noi
matematici, quando dimostriamo un teorema, sappiamo che sarà valido per sempre.
Ma in concreto, quando finiamo di scrivere la dimostrazione, esiste sempre il
dubbio: ci sarà qualche errore nei ragionamenti? Il nostro sistema di
pubblicazione e diffusione dei risultati stabilisce vari filtri per cui il
testo deve passare prima che sia considerato corretto e venga incluso nella
letteratura scientifica: rivediamo il lavoro nel dettaglio; lo spieghiamo ai
colleghi, cercando di convincerli della sua validità; esponiamo i nostri
risultati su Internet dove tutti i matematici possono vederli; mandiamo
l’articolo a una rivista scientifica in cui il direttore, prima di pubblicarlo,
lo invia a qualche esperto di quel campo, il cui compito è verificare che non
ci siano errori, oltre che di valutare se il risultato è sufficientemente
interessante per la pubblicazione.Tuttavia, benché possa risultare inquietante,
questi processi non sono infallibili, e a volta lasciano passare risultati
scorretti”. Nel 1998, il matematico Carlos Simpson espresse dubbi su un teorema
enunciato nel 1989 da Vladimir Voevodsky poiché una dimostrazione non lo
soddisfaceva, ma era talmente complessa che Simpson non fu capace di trovare
l’errore. Fu lo stesso Voevodsky che lo individuò nel suo ragionamento, ma solo
nel 2013. Nel 2000, trovarono un altro errore in un altro dei suoi lavori, che
dalla pubblicazione nel 1993 era stato studiato e validato dagli esperti. Ciò
produsse una profonda impressione in Voevodsky, che decise di abbandonare per
il momento le sue indagini abituali e dedicarsi a cercare una maniera di
comprovare automaticamente i ragionamenti matematici per individuare gli errori
nascosti nelle dimostrazioni.
Dal cervello alla macchina
"Si può scrivere qualsiasi
dimostrazione, partendo da alcune ipotesi e seguendo regole logiche ben
definite, in modo che una macchina potrebbe controllare la validità di ogni
passaggio. In pratica però - osserva Tomás Gómez - questo non è possibile,
poiché le ipotesi su cui si fondano le matematiche sono la teoria degli
insiemi, e questa è così remota dal tipo di argomenti che si impiegano nella
ricerca effettiva che formalizzare una dimostrazione fino all’ultimo
particolare sarebbe un lavoro improbo, impossibile da realizzare. Ma… se ci
fosse un’altra teoria su cui si potessero fondare le matematiche e con la quale
fosse fattibile scrivere dimostrazioni che una macchina possa
controllare?" Ci sono stati tentativi in questa direzione, sostituendo la
teoria degli insiemi con la teoria dei tipi, perseguendo idee che derivano
dall’informatica teorica. Nel 2012, lo staff guidato da Georges Gonthier mise a
punto una dimostrazione comprovabile da un computer del teorema di
Feit-Thompson, un importante risultato della teoria dei gruppi del 1963.
Voevodsky incorporò concetti di topologia e geometria algebrica nella teoria
dei tipi. Voevodsky integrò il computer nel processo di ricerca, descrivendolo
– si ricorda sul 'New York Times' – un po’ come un videogame: “Tu dici al
computer ‘Prova questo’, e lui lo prova, e ti restituisce il risultato delle
sue azioni”, spiegò in una intervista del 2013. “Certe volte quel che viene
fuori da questo è inaspettato. E’ divertente”. Sarebbe un’autentica rivoluzione
se si riuscisse a trovare un sistema sufficientemente semplice da essere
impiegato dai matematici. Oltre a evitare il problema degli errori nascosti,
libererebbe dalla fatica del controllo e della revisione. Nato il 4 giugno 1966
a Mosca, Voevodsky era figlio di Alexander, direttore di un laboratorio di
fisica sperimentale all’Accademia delle Scienze russa, e di Tatyana
Voevodskaya, docente di Chimica all’Università di Mosca. Dopo la caduta del
Muro di Berlino, fece il dottorato a Harvard e ottenne un posto permanente
all'Institute for Advanced Study a Princeton. Nel 2002 ottenne la medaglia
Fields, uno dei più prestigiosi premi nelle matematiche, con la motivazione che
il suo lavoro ”è caratterizzato da un'abilità formidabile nel gestire idee
altamente astratte e di utilizzare con facilità e flessibilità queste idee per
risolvere problemi matematici alquanto concreti."
_copertina_fronte_(500x771).jpg)
_ISBN_(200x308).jpg)
