(con Marco Maggesi e Alberto Mancini, Università degli Studi di Firenze)

I metodi formali permettono di comporre automaticamente le dimostrazioni al computer di teoremi di matematica, permettendo di fatto a più matematici di unire gli sforzi (in modo asincrono) verso obiettivi più ambiziosi.

Tali metodi sono ancora più importanti alla luce di risultati notevoli ottenuti di recente (cfr. http://www.ams.org/notices/200811/) e anche di progetti di enormi dimensioni (i.e. https://code.google.com/p/flyspeck/) che cercano di dare risposta a delle sfide sinora inedite (Why give a formal proof of the Kepler Conjecture?)

In questo talk mostreremo come sia possibile implementare, usando PostgreSQL, una infrastruttura per la certificazione collaborativa di teoremi matematici basata sulle transazioni ACID, i linguaggi procedurali e le query ricorsive, e dotata di una interfaccia web versatile che incoraggia ulteriormente il lavoro di gruppo anche tramite dispositivi mobili quali i tablet.