Congettura di Keplero o teorema di Hales?

Impacchettamento delle sfere

Problema

Sistemare delle sfere nello spazio euclideo in modo che la densitamedia sia maggiore possibile.

Impacchettamento cubico e impacchettamento esagonale

Congettura di Keplero o teorema di Hales?

Enunciato delle congettura

E facile vedere che le sfere possono essere impacchettate con unadensita media, pari a

π√18

� 0.74048.

Congettura di Keplero

Nessun altro metodo di impacchettamento permette di ottenereuna densita media superiore.

Congettura di Keplero o teorema di Hales?

Storia del problema

� 1611: Keplero formula la congettura.

� 1831: Gauss dimostra la congettura per “reticoli regolari”.

� 1900: Hilbert include la congettura nella sua famosa lista di23 problemi.

� 1953: Laszlo Fejes Toth riduce la congettura ad un numerofinito di problemi risolvibili per calcolo diretto.

� 1993 Wu-Yi Hsiang: dimostrazione della congettura, ma gliesperti ritengono che le sue argomentazioni siano insufficienti.

� 1998 Thomas Hales: dimostrazione della congettura con unforte uso del computer sulla traccia di Fejes Toth.

� 2003: La parte teorica della dimostrazione viene pubblicata suAnnals of Mathematics.

� 2003: Hales annuncia il progetto FlysPecK (tuttora in corso).

Theorema di Feit e Thompson

� Teorema (Feit–Thompson 1963): Ogni gruppo di ordinedispari e risoluble.

� Statistiche sulla dimostrazione (250 pagine su 300 pagine diprerequisiti).

� E una delle prime tappe significative verso il teorema diclassificazione dei gruppi semplici finiti (circa 5.000 pagine).

� E stato uno dei primi esempi di dimostrazione lunga in teoriadei gruppi.

Statistiche sulla formalizzazione intera

� Statistiche sulla formalizzazione intera� Formalizato al computer il 20 settembre 2012 dopo un lavoro di

6 anni di un intero team congiunto INRIA-Microsoft Research.� Lines of code : ∼170.000� Number of definitions : ∼4200� Number of theorems : ∼15.000

� Statistiche sulla formalizzazione piu propriamenteriguardante il teorema.

� Lines of code : ∼47.000 (∼30%)� Number of definitions : ∼200 (∼5%)� Number of theorems : ∼1.300 (∼10%)

Cappelli messicani e reflection

� L’idea e quella di superare la logica dei cappelli messicani.

� Il progetto pero sviluppa una teoria dei gruppi valida soltantoper i gruppi finiti.

� Il progetto punta molto su di una tecnica chiamata“reflection” (piu particolarmente small scale reflection. Checerca di sfruttare al massimo la capacita del computer di”calcolare” la dimostrazione.

HoTT e Univalent Foundation

Teoria dei tipi

� La teoria dei tipi risale a Russell (a cavallo 1900).

� Fondamento alternativo alla teoria degli insiemi (alla base lastessa idea intuitiva di ”aggregato”).

� Svolta negli anni ’70 con Intuitionistic Type Theory di PerMartin Lof.

� Vengono sviluppati vari dimostratori di teoremi (NuRPL, Coq,Agda) basati su ITT e altri formalismi derivati (CIC).

HoTT e Univalent Foundation

Teoria dell’omotopia

� Origine in topologia (definizione classica conosciuta da tutti).

� Con la topologia algebrica si propaga all’algebra omologica ealle strutture discrete (insiemi simpliciali).

� Quillen nel ’67 propone una ”teoria assiomatica”dell’omotopia: (Closed) Model Category.

� L’omotopia viene successivamente riconosciuta come uno deifenomeni fondamentali pervasivi della matematica. Siriconosce la natura omotopica di altri fenomeni, ad esempionella geometria algebrica (Vladimir Voevodsky, Fields 2002).

HoTT e Univalent Foundation

Seppie con i piselliSi sono rivelate (Awodey, Voevodsky et al.) alcune interazioniinaspettate tra ITT e Ho.

� Esiste un modello omotopico di CIC.

� Esiste una struttura omotopica su CIC.

Quindi possiamo usare CIC per dimostrare teoremi validi in Ho epossiamo usare Ho per capire meglio CIC.Nuova fondazione della matematica (Univalent Foundation).Anno speciale all’IAS.

Chi controlla il controllore?

Perche dovremmo credere che una dimostrazione verificata alcomputer sia piu affidabile di una dimostrazione fatta a mano oprodotta da un programma ad-hoc?

� La logica del dimostratore potrebbe essere inconsistente.(Anche i logici piu famosi hanno proposto sistemi che si sonosuccessivamente rivelati essere inconsistente).

� Le regole d’inferenza potrebbero essere implementateincorrettamente.

� I software di dimostrazione assistita sono spesso programmimolto complessi.

Prima risposta: a chi importa?

E estremamente improbabile in pratica che un bug produca unadimostrazione ‘apparente’.

Anche il piu fragile dimostratore di teoremi si rivela piu affidabile diun essere umano nella maggior parte dei casi.

Problemi nella specifica e nella modellizzazione sono molto piufrequenti.

La certezza assoluta non esiste comunque.

Seconda risposta: forse ci importa

Ci sono stati alcuni esempi (anche se rari) di dimostrazioniapparenti.

Se richiediamo rigore matematico dobbiamo anche pretendererigore nello sviluppo dei dimostratori di teoremi.

Una dimostrazione formale serve proprio per accertare un fattomatematico al di la di ogni dubbio.

La perfezione e irraggiungibile ma vale comunque la pena diricercarla.

Architettura dei dimostratori di teoremi

Criterio di de Bruijn:

l’affidabilita di un verificatore di teoremi deve dipenderesolo dalla correttezza di un nucleo minimale.

Il nucleo che verifica una dimostrazione puo essere molto piupiccolo dell’intero dimostratore.

Esempio (HOL Light):

� 10 regole di inferenza

� 3 assiomi

� 430 linee di codice per l’implementazione del nucleo

Uso degli oracoli

Idea:

� usare un programma dedicato (es. CAS) per trovare ladimostrazione.

� usare un verificatore di teoremi per validare la dimostrazione.

Conclusioni

� La formalizzazione della matematica e possibile.

� Ha gia trovato importanti applicazioni in pratica.

� Potrebbe rivelarsi molto utile anche in matematica pura.

� Non e ancora emerso uno standard capace di affermarsi.