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.
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.
Nessun commento:
Posta un commento