Matematica al computer

Può un computer dare una dimostrazione di un teorema?

Con un piccolo aiuto sì!

Le Mathematics Mechanization and Automated Reasoning Platform (per gli amici MMP) sono dei software sviluppati nel corso degli anni per risolvere autonomamente alcuni lemmi e teoremi principalmente algebrici e geometrici.

Il processo di Meccanizzazione della Matematica consiste nel verificare in modo algoritmico tramite un computer una dimostrazione formale. Per formale si intende una dimostrazione scritta in linguaggio puramente simbolico e che quindi il software può controllare partendo da alcuni assiomi preimpostati e dai teoremi precedentemente dimostrati (attraverso lo stesso software).

Attualmente, la tecnologia consente solo un sistema di dimostrazione interattiva in cui un matematico collabora con la macchina e fa la maggior parte del lavoro. La dimostrazione (o confutazione) totalmente automatica di teoremi si limita a pochi casi.

In pratica, nessun testo di matematica, ad esclusione probabilmente dei soli Principia Mathematica di Russell e Whitehead è scritto in linguaggio logico totalmente formale.

Dunque per utilizzare questo nuovo (non così tanto come leggerete tra poco) mezzo a disposizione dei matematici è necessario imparare un codice molto simile ai linguaggi di programmazione come il C e il Pascal.

La dimostrazione di "1+1=2" in una pagina del libro di B. Russell e A. N. Whitehead 

Una rapida storia della meccanizzazione della matematica:

• 1910
• I Principia Mathematica (che trovate online qui) di Bertrand Russel e Alfred North Whitehead vengono pubblicati: sono oltre 1000 pagine di puri simboli che raggiungono un risultato significativo solo a pagina 162: $ 1+1=2 $.
• 1967
• Nasce Automath: il primo linguaggio per la scrittura formalizzata di definizioni e dimostrazioni matematiche, creato dal matematico olandese Nicolaas de Bruijn.
• 1973
• Il polacco Andrzej Trybulec lancia Mizar. Oggi la libreria Mizar contiene oltre 8 mila definizioni e 46 mila teoremi.
• 1977
• L. S. Jutting formalizza il libro di Landau in Automath. (lo trovate qui)
• 1976
• Teorema dei 4 colori: la congettura che una mappa (qualsiasi!) possa essere colorata utilizzando solamente 4 colori diversi è formulata nel 1852. Varie dimostrazioni e smentite si susseguono fino al 1976, quando Appel e Hanken annunciano di avere una prova che però richiede una verifica al computer. Nel 2005 Gontier meccanicizza completamente il teorema in Coq.
• 2005

• Un team di matematici utilizza il sistema Mizar per dimostrare il Teorema della curva chiusa di Jordan. Il teorema in apparenza ovvio afferma pressappoco che: Una curva piana semplice chiusa divide il piano in due regioni: una "interna" ed una "esterna". 
• 1986
• I Teoremi di Incompletezza di Goedel sono stati formalizzati tramite il dimostratore Boyer-Moore.
• 2012
• Dopo 6 anni di lavoro è meccanizzato anche il Teorema di Feit-Thompson il cui enunciato molto semplice è: Tutti i gruppi finiti sono risolubili. Enunciato nel 1911 e dimostrato in ben 255 pagine più di cinquant'anni dopo. 
• 2014

• Il Teorema di Hales (meglio noto sotto il nome di congettura di Keplero) è ufficialmente dimostrato. 403 anni prima Keplero si chiedeva quale fosse il modo per impilare delle sfere occupando il minor spazio possibile. Tra gli altri, Gauss si cimentò nella dimostrazione, ottenendo alcuni risultati particolari. Nel 1900 Hilbert lo include nella sua lista di 23 problemi del secolo; mezzo secolo più tardi Fejes Toth riduce la dimostrazione al controllo di un numero (enorme ma) finito di casi. Solo nel 1998 Hales dà la sua dimostrazione ottenuta in gran parte grazie all'utilizzo di un computer.

Un video sul teorema dei 4 colori

Quali sono i problemi riguardo questo processo dimostrativo?

1. Non tutti i teoremi possono essere dimostrati attraverso il linguaggio della logica (a causa del limite teorico imposto dai teoremi di Godel).
2. Come essere sicuri che gli eventuali bug dei software non abbiano influito sul risultato ottenuto?
3. È realmente utile dimostrare al computer teoremi ormai consolidati da secoli?
4. Quante risorse - umane, di calcolo, di tempo - richiede una simile formalizzazione e realizzazione?

Risposte veloci alle questioni e alle domande poste:

1. I già citati Principia Mathematica sono la prova di come il linguaggio astruso della logica possa descrivere gli enunciati e le dimostrazioni. (con non poca fatica...!)
2. Non si ha mai la certezza assoluta. Ma si può usare un debugger per controllare. Dato che ci sono differenti software utilizzati, lo stesso risultato ottenuto con più di un software aumenta la probabilità di correttezza. Infine, anche le dimostrazioni svolte a mano non sono esenti da errori. Alcuni celeberrimi matematici sono caduti in trappole logiche, e gli errori più famosi sono raccolti ad esempio nel libro di Maurice Lecat, Erreurs de Mathématiciens des origines à nos jours (1935) (se vi interessa lo trovate qui).
3. L'unico modo per rendere utile questo strumento nel prossimo futuro è di fargli apprendere il maggior numero di teoremi e risultati possibile, così da risparmiare - si spera - fatica in seguito. Inoltre ci sono dimostrazioni che richiedono calcoli impossibili da eseguire a mano, altre particolarmente lunghe e complicata che necessitano di una attenzione prolungata, o altre ancora molto tecniche che sono perfette da dare in pasto ad un calcolatore. 
4. Ormai è stato meccanizzato il contenuto di Analisi, Algebra Lineare, Logica, e molti altri settori importanti, corrispondente circa a quello svolto nei primi due o tre anni di università di Matematica.I principali dimostratori attualmente in uso sono Coq, HOL Light, HOL4, Isabelle, Idris, Mizar, ProofPower, PVS, Nuprl. Sfortunatamente sono tutti incompatibili tra loro: un teorema provato su Mizar non può essere utilizzato in Coq (o uno qualunque degli altri). 

Per di più i costi della meccanizzazione sono ancora molto alti al giorno d'oggi. Tuttavia i software di controllo e certificazione di protocolli che stabiliscono il corretto funzionamento di un dispositivo si basano proprio su queste tecnologie, e dato il loro sempre più frequente utilizzo, il costo si dovrebbe abbassare significativamente nei prossimi anni.



Per saperne di più sugli obiettivi che la matematizzazione della matematica si pone, potete leggere il QED Manifesto.