L’imprenditore tecnologico e pioniere della blockchain, Charles C. Hoskinson, meglio conosciuto come il fondatore di Cardano e il co-fondatore di Ethereum, due delle reti di criptovalute più famose al mondo, ha donato 20 milioni di dollari per creare l’Hoskinson Center for Formal Mathematics nel Dietrich College of Humanities and Social Sciences presso la Carnegie Mellon University, che svilupperà nuove tecnologie per il cosiddetto “theorem proving”.
La ricerca sul theorem proving
L’Hoskinson Center for Formal Mathematics sarà guidato dal dr. Jeremy Avigad, professore di filosofia al Dietrich College e di scienze matematiche al Mellon College of Science (MCS), che fornirà tutoraggio e guida ai contributi diretti alla ricerca. Il centro svilupperà nuove tecnologie per facilitare l’enunciazione di teoremi matematici in modo che i computer possano aiutare a scoprire dimostrazioni, verificare passaggi e certificare la correttezza (“theorem proving”). Abilitando un nuovo modo di fare matematica e creando librerie digitali collaborative per questi strumenti matematici si vuole rendere questa tecnologia ampiamente accessibile e far progredire le scoperte in un’ampia gamma di discipline, tra cui informatica, intelligenza artificiale, fisica, economia. Il centro lavorerà in stretta collaborazione con docenti, studenti e ricercatori in tutto il campus, in particolare nel Dipartimento di Scienze Matematiche all’interno di MCS e nella School of Computer Science.
Nel settembre 2011, il Dietrich College of Humanities and Social Sciences aveva già ricevuto da William S. Dietrich II, uomo d’affari, studioso, filantropo e fiduciario di lunga data della Carnegie Mellon University, un piano per una donazione record di un fondo di 265 milioni di dollari per sostenere la stessa università. Il fondo doveva fungere da catalizzatore per le iniziative globali dell’università e per la fusione del pensiero dell’emisfero sinistro e dell’emisfero destro, come gli studi che collegano la tecnologia e le arti, nonché il supporto per future iniziative accademiche in tutta l’università, compresi programmi per studenti universitari e laureati, borse di studio, creazione artistica e ricerca.
Il dimostratore di teoremi Lean di Microsoft
“Consentendo un nuovo modo di fare matematica e creando librerie digitali collaborative per strumenti matematici, possiamo accelerare le scoperte in un’ampia gamma di discipline. Questo centro è una chiara espressione dei nostri punti di forza nella collaborazione e nella sperimentazione guidata dalla tecnologia, sono entusiasta del suo potenziale”, ha affermato il direttore del Centro, Jeremy Avigad.
Situata all’incrocio tra filosofia, matematica e informatica, la “matematica formale” lavora su teoremi e dimostrazioni matematiche dopo che sono stati enunciati in un linguaggio formale, che a sua volta consente di sviluppare programmi per computer per aiutare a scoprire dimostrazioni, verificando i passaggi umani inserire, e certificando la correttezza di ogni prova che possa essere così formalizzata (theorem proving). L’Hoskinson Center svilupperà la tecnologia tramite la piattaforma Lean, un dimostratore di teoremi e un linguaggio di programmazione della Microsoft, basato sul calcolo delle costruzioni con tipi induttivi. Il progetto Lean è un progetto open source, ospitato su GitHub, una piattaforma software sviluppata da Microsoft Research.
Il Centro sosterrà anche lo sviluppo della biblioteca digitale di Lean, svilupperà nuovi strumenti per aiutare a convertire le dichiarazioni matematiche dal linguaggio naturale a un linguaggio formale e creerà risorse educative per rendere questi strumenti ampiamente disponibili. Utilizzati ampiamente, questi strumenti hanno il potenziale per potenziare la matematica, che a sua volta ha il potere di potenziare l’informatica, la fisica e qualsiasi altra disciplina che utilizza la matematica.
“Possiamo riunire le migliori menti in matematica, informatica e apprendimento automatico per creare un’infrastruttura per l’utilizzo della matematica formale come strumento educativo fondamentale. Sono onorato di far parte della creazione di un centro così importante in cui collaborazione, esplorazione e scoperta aprono le porte per incentivare e supportare l’attività matematica e dotarla delle risorse per metodi avanzati di automazione”, ha affermato il professor Avigad.
Il filantropo Hoskinson, con una vasta esperienza con la matematica e la tecnologia, vede il potenziale globale dei metodi formali, incluso lo sviluppo di una biblioteca matematica digitale comune, nel rendere la matematica accessibile a una comunità più ampia.
“Gli assistenti di dimostrazione computazionale basati sulla matematica formale sono una tecnologia trasformativa”, afferma Avigad. “Non solo ci aiutano a garantire che la matematica che svolgiamo sia corretta, ma forniscono anche nuovi potenti strumenti per la comunicazione, la collaborazione, l’istruzione e la scoperta matematica”.
Matematica e analisi scientifica
“La matematica è essenziale per la scoperta e l’analisi scientifica. Portare i più recenti strumenti abilitati dalla tecnologia ai nostri ricercatori e studenti migliorerà la nostra visione per creare il futuro della scienza”, afferma Rebecca W. Doerge, Glen de Vries Dean del Mellon College of Science. “La comunità del Mellon College of Science, incluso il nostro dipartimento di scienze matematiche di alto livello, è entusiasta di collaborare a questo Centro, mentre continuiamo a portare avanti il campo della matematica in modo veramente interdisciplinare”.
La donazione è l’impegno più recente come parte di “Make Possible: The Campaign for Carnegie Mellon University”. I sostenitori della campagna stanno accelerando le ambiziose priorità strategiche dell’università, con l’obiettivo di raccogliere 2 miliardi di dollari tramite la filantropia privata per le iniziative nei suoi sette college e scuole. Obiettivo quasi centrato, visto che, a oggi, hanno contribuito più di 52mila sostenitori con oltre 1,75 miliardi di dollari.
