01 ottobre 2008

Wiki per una Matematica Formalmente Verificata

Leggo su Slashdot la proposta di alcuni matematici del MIT di creare un wiki specifico per la matematica, che contenga tutte le dimostrazioni dei teoremi esistenti e che sia in grado di verificare formalmente la correttezza di quello che è scritto.
Slashdot | Towards a Wiki For Formally Verified Mathematics

Nella matematica formale è molto più complesso trovare nuovi teoremi significativi (utili) che verificare la correttezza dei teoremi esistenti. In pratica, dato un teorema formale e una dimostrazione un programma può verificare automaticamente se la dimostrazione è corretta e quindi se il teorema è vero.

Vdash.org ha due interessanti slides che spiegano il progetto:
Slides from MIT E-Club talk (Aug 11, 2008)

Slides from O'Reilly Ignite Boston 4 talk (Sep 11, 2008)

Il progetto prevede di poter scrivere i teoremi e le dimostrazioni da inserire nel wiki in Latex e che il software del wiki sia in grado di verificare, prima di pubblicare, la correttezza della dimostrazione. Il tutto basandosi su software opensource e usando la licenza BSD per il contenuto del wiki.

Sarebbe una nuova risorsa molto importante a disposizione del pubblico e degli addetti ai lavori.

Interessante una citazione presente nelle slides:

"We are not scanning all those books to be read by people,"
explained one of my hosts after my talk. "We are scanning
them to be read by an AI."
 -George Dyson, on his visit to Google, 2005.
Posta un commento