C hi era Vladimir Voevodsky, il genio russo della matematica morto a cinquantun anni a Princeton, nel cui prestigioso Istituto insegnava? 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. Il 'New York Times' lo ha 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.
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.
"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."