Lean: un forum collaborativo ----------------------------
L’idea è semplice: formalizzare tutte le conoscenze matematiche in un assistente di prova libero e aperto chiamato Lean (****).
Lean è dunque un software che permette di verificare dimostrazioni matematiche. Programmi di questo tipo sono stati utilizzati per la dimostrazione del teorema dei quattro colori (vedi i Grafi, Biblioteca Tangente 54, 2015) e per la congettura di Keplero sull’impacchettamento delle sfere (vedi Tangente 158, 2014). Uno degli assistenti di prova più usati è Coq, sviluppato dall’Inria.
Lean è sviluppato da Microsoft Research in C++ (Leonardo de Moura, 2013). Attualmente è usato, fra gli altri, da Thomas Hales, colui che ha risolto la congettura di Keplero.
A questo scopo, gli utenti si riuniscono su un forum online chiamato Zulip (****). Per iniziare, devono prendere confidenza con i vari strumenti e abituarsi a modalità di lavoro diverse da quelle consuete; il loro primo obiettivo è digitalizzare il programma del primo ciclo di studi. Metà del lavoro è già stata svolta. In questo caso, «digitalizzare» non significa «scansionare documenti», bensì introdurli in Lean in un formato comprensibile al software. Il vantaggio è che Lean verifica che la dimostrazione proposta sia valida e coerente con le regole della logica e gli assiomi implementati.