La matematica su nuove basi

Si prospetta una vera e propria rivoluzione della matematica? Una rivoluzione che cambierà radicalmente il modo di lavorare della matematica? Nel prossimo futuro i computer, anziché gli esseri umani, verificheranno in modo affidabile la correttezza di una prova matematica?

Secondo la blogger Julie Rehmeyer, il matematico russo Vladimir Voevodsky (*1966), professore all'Institute for Advanced Studies di Princeton, ha sviluppato un approccio che potrebbe rivoluzionare la matematica e i suoi fondamenti: In linea di principio, il matematico russo è riuscito a dimostrare che la teoria dell'omotopia, che si occupa della deformazione degli oggetti geometrici, esprime le stesse idee della teoria dei linguaggi di programmazione e della logica matematica, solo in un linguaggio diverso (la teoria dell'omotopia ha avuto un ruolo centrale nel lavoro del russo sulla congettura di Milnor).sulla congettura di Milnor, per la quale è stato insignito della prestigiosa medaglia Fields nel 2002), scrive in un blog della rivista di divulgazione scientifica "Scientific American".

Lo stesso Wojewodski vuole unire due filoni di sviluppo della matematica moderna. L'ETH di Zurigo lo ha invitato come relatore alle "Paul Bernays Lectures 2014" che si terranno a settembre, in modo che possa presentare le sue idee di persona a Zurigo. Giovanni Felder, capo dell'Istituto di studi teorici dell'ETH (ETH-ITS), presenterà le sue ricerche al pubblico dell'ETH. Wojewodski sta sviluppando una nuova teoria che pone la matematica su una nuova base. Questa teoria si chiama "Homotopy Type Theory (HoTT)" e "Univalent Foundations of Mathematics" è il progetto associato orientato all'informatica.

Un linguaggio più semplice per le prove informatiche

Nell'ambito di "HoTT", Wladimir Wojewodski sta sviluppando un approccio con il quale le prove matematiche possono essere tradotte in un linguaggio di programmazione per gli assistenti di prova del computer in modo molto più semplice rispetto a oggi. Se questo approccio avrà successo, in futuro i computer potrebbero essere in grado di verificare anche prove complicate, in cui anche matematici altamente qualificati commettono errori. "Con l'aiuto degli assistenti di prova per computer, potremmo formare teorie matematiche molto complesse e molto astratte", afferma Wojewodski.

Per i matematici, questi assistenti alla prova non sarebbero una questione secondaria, perché da un lato la prova è qualcosa di simile alla loro tecnica chiave, e dall'altro gli assistenti alla prova richiedono nuovi fondamenti della matematica. In primo luogo, per essere accettate, le prove in matematica devono essere corrette e rispettare le regole logiche. Deve essere possibile dedurre la loro correttezza senza errori e a partire da alcuni principi veri (assiomi) e da affermazioni già dimostrate. Il sogno di molti matematici è sempre stato quello di formulare assiomi dai quali tutti i teoremi matematici possano essere derivati e dimostrati senza contraddizioni.

La teoria degli insiemi è difficile da tradurre

Ernst Zermelo presentò questo sistema di assiomi nel 1908. Oggi è noto come sistema assiomatico Zermelo-Fraenkel della teoria degli insiemi e costituisce il fondamento di tutta la matematica, poiché tutti gli oggetti matematici possono essere interpretati come insiemi.

Lo svantaggio della teoria degli insiemi è che i suoi principi sono molto difficili da tradurre nel linguaggio di programmazione di un assistente di dimostrazione. I programmi di dimostrazione oggi esistenti, come il "coq" utilizzato da Wojewodski, si basano sulla teoria dei tipi, che il matematico e filosofo inglese Bertrand Russell (1872-1970) propose come alternativa alla teoria degli insiemi.

L'aspetto innovativo dell'approccio di Wojewodski è che egli interpreta gli enunciati del sistema formale della teoria dei tipi nel linguaggio della teoria dell'omotopia. In questa interpretazione si applica una proprietà aggiuntiva, la cosiddetta univalenza, che Wojewodski aggiunge come nuovo assioma ai fondamenti della matematica. In esso, egli mette in relazione l'uguaglianza degli enunciati logico-matematici con l'equivalenza nel senso della teoria dell'omotopia.

Tazza e ciambella: un linguaggio più ricco

Questo approccio può sembrare inizialmente sorprendente, perché la teoria dell'omotopia si occupa in realtà di come oggetti geometrici diversi possano essere trasformati l'uno nell'altro attraverso le deformazioni. Ciò può essere illustrato utilizzando una tazza e una ciambella: in termini di forma, i due oggetti sembrano completamente diversi. In termini di proprietà, però, sono entrambi un "oggetto con un'apertura". La ciambella è un anello e la tazza ha un manico. Inoltre, la tazza può essere trasformata in una ciambella in modo tale che i punti vicini sulla tazza siano anche vicini sulla ciambella. I due oggetti, intuitivamente diversi, hanno quindi le stesse proprietà. Sono equivalenti o equivalenti, come dicono i matematici.

Il problema dell'equivalenza si pone anche nell'interpretazione delle equazioni utilizzate in matematica e nei linguaggi di programmazione. Un'equazione come "a=b" è un'affermazione matematica in cui due simboli diversi hanno lo stesso valore. Ciò corrisponde logicamente a due forme diverse con proprietà strutturalmente identiche.

Stessa idea, lingue diverse

"Grazie a Wojewodski, ora sappiamo che queste relazioni di uguaglianza possono essere formulate meglio nella teoria dell'omotopia, che è una teoria più ricca", afferma Giovanni Felder. La teoria dell'omotopia non solo spiega perché "a è uguale a b", ma anche come si arriva da a a b. Nella teoria degli insiemi, queste informazioni dovrebbero essere definite in aggiunta, il che rende difficile tradurre frasi matematiche in linguaggio di programmazione, dice Felder: "La speranza è che con il metodo di Wojewodski si possano tradurre le prove più direttamente nel linguaggio di programmazione e verificarle in modo più efficiente".

Alla domanda se in futuro i computer prevarranno sull'uomo nella verifica delle prove matematiche, Wojewodski e Felder si dichiarano in apertura. Wojewodski afferma: "Siamo ancora all'inizio di un lungo percorso di cambiamento, ed è impossibile dire oggi dove ci porterà". Felder afferma: "I computer possono commettere errori. Le persone possono sbagliare. L'unica certezza è che la matematica diventerà più complessa e dimostrarla non diventerà più facile".