Congettura di Keplero

In matematica la congettura di Keplero è una congettura riguardante l'impacchettamento di sfere nello spazio euclideo tridimensionale. Essa afferma che non esiste alcun modo di sistemare delle sfere nello spazio con densità media superiore a quella dell'impacchettamento cubico a facce centrate o a quella dell'impacchettamento esagonale. La densità di questi due modi di sistemare le sfere è leggermente maggiore del 74%.

Nel 1998 Thomas Hales, attualmente professore all'università di Pittsburgh, annunciò di possedere una dimostrazione della congettura di Keplero. La sua dimostrazione è fatta per esaustione e prevede di controllare molti casi singoli mediante complessi calcoli al computer. I referee, dopo aver letto l'articolo, annunciarono di essere certi "al 99%" della correttezza della dimostrazione di Hales. La dimostrazione formale della congettura di Keplero è stata completata e verificata nel 2014.

Il problema

Un esempio di impacchettamento cubico: 35 sfere formano un tetraedro.

Due modi per sovrapporre tre strati di sfere.

Si immagini di riempire un contenitore con piccole sfere, tutte della stessa dimensione. La densità dell'impacchettamento è la percentuale di volume del contenitore che viene occupata dalle sfere. Per massimizzare il numero di sfere nel contenitore è necessario trovare un modo di sistemare le sfere che possieda la densità massima, in modo tale che le sfere vengano impacchettate il più vicino possibile una all'altra.

Mediante prove sperimentali si è visto che, se si fanno cadere le sfere casualmente all'interno del contenitore, si ottiene una densità intorno al 65%. Si può però ottenere una densità maggiore cercando di sistemare le sfere accuratamente nel modo seguente. Si inizia con uno strato di sfere disposte secondo una griglia esagonale, poi si mette un nuovo strato di sfere nei punti più bassi che si possono trovare sopra al primo strato, e così via. Questo metodo naturale di impilare le sfere crea uno dei due impacchettamenti simili chiamati impacchettamento cubico e impacchettamento esagonale. Questi due metodi hanno entrambi una densità media uguale a

${\frac {\pi }{\sqrt {18}}}\simeq 0{,}74048.$

La congettura di Keplero afferma che non si può fare di meglio: nessun altro impacchettamento di sfere può avere una densità superiore.

Origini

La congettura prende il suo nome da Giovanni Keplero, che la enunciò nel 1611 in Strena seu de nive sexangula (Sul fiocco di neve a sei angoli). Keplero iniziò a studiare le sistemazioni di sfere in seguito a uno scambio di corrispondenza con il matematico e astronomo inglese Thomas Harriot nel 1606. Harriot fu amico e assistente di Walter Raleigh, che assegnò proprio ad Harriot il problema di determinare il modo migliore per sistemare le palle di cannone sui ponti delle sue navi. Harriot pubblicò uno studio di diversi metodi di impacchettamento nel 1591, e in seguito proseguì i suoi studi cercando di sviluppare una delle prime teorie atomiche.

Diciannovesimo secolo

Keplero non possedeva una dimostrazione della congettura, e il passo successivo sulla via della dimostrazione fu fatto dal matematico tedesco Carl Friedrich Gauss, che pubblicò una soluzione parziale nel 1831. Gauss dimostrò che la congettura di Keplero è vera se le sfere devono essere sistemate secondo una griglia regolare. Ciò significava che qualunque configurazione di sfere che fornisse un controesempio alla congettura di Keplero avrebbe dovuto essere irregolare. Ma l'eliminazione di tutti i possibili impacchettamenti irregolari è molto difficile, e questo è il motivo per cui la congettura è così difficile da dimostrare.

In effetti, esistono impacchettamenti irregolari che sono più densi di quello cubico in un volume sufficientemente piccolo, ma ogni tentativo di estenderli a volumi maggiori riduce sempre la loro densità. Dopo Gauss, nel diciannovesimo secolo non furono fatti ulteriori progressi nella dimostrazione della congettura di Keplero. Nel 1900 David Hilbert la incluse nella sua lista di ventitré problemi non risolti della matematica, nota come problemi di Hilbert: essa forma parte del diciottesimo problema.

Ventesimo secolo

Il passo successivo verso una soluzione fu fatto dal matematico ungherese László Fejes Tóth. Nel 1953 Fejes Tóth mostrò che il problema di determinare la massima densità di tutte le disposizioni di sfere, regolari ed irregolari, poteva essere ridotto a un numero finito, anche se molto grande, di calcoli. Questo significava che era possibile, almeno in linea di principio, trovare una dimostrazione per esaustione. Un computer sufficientemente potente avrebbe potuto fornire un approccio pratico alla risoluzione del problema. Nel frattempo vennero fatti tentativi per trovare un estremo superiore per la massima densità di un qualunque impacchettamento di sfere. Il matematico inglese Claude Ambrose Rogers stabilì un limite superiore di circa 78% nel 1958, e tentativi successivi fatti da altri matematici ridussero leggermente questo valore, che era comunque di molto superiore alla densità dell'impacchettamento cubico, cioè 74%.

Furono anche prodotte dimostrazioni errate. L'architetto e geometra statunitense Richard Buckminster Fuller affermò di essere in possesso di una dimostrazione nel 1975, ma si scoprì poco dopo che non era corretta. Nel 1993 Wu-Yi-Hsiang, all'Università della California - Berkeley pubblicò un articolo in cui affermava di aver dimostrato la congettura di Keplero usando metodi geometrici. Alcuni esperti affermarono di non aver trovato motivazioni sufficienti per alcune delle sue affermazioni. Sebbene non si fosse trovato alcunché di scorretto nel lavoro di Hsiang, la maggioranza dei matematici si trovò d'accordo nell'affermare che la dimostrazione di Hsiang era incompleta. Uno dei critici più attivi fu Thomas Hales, che all'epoca stava lavorando a una sua dimostrazione.

La dimostrazione di Hales

Seguendo l'approccio suggerito da László Fejes Tóth, Thomas Callister Hales, all'epoca all'Università del Michigan, determinò che la massima densità di tutti gli impacchettamenti poteva essere trovata minimizzando una funzione di 150 variabili. Nel 1992, assistito dal suo studente di dottorato Samuel Ferguson, diede inizio a un programma di ricerca per applicare sistematicamente i metodi della programmazione lineare alla ricerca di un limite inferiore per il valore di questa funzione relativo a un insieme di più di 5000 differenti configurazioni di sfere. Se, per ognuna di queste configurazioni, fosse riuscito a trovare un limite inferiore che fosse maggiore del valore relativo all'impacchettamento cubico, allora la congettura di Keplero sarebbe stata dimostrata. La ricerca di tutte queste limitazioni inferiori avrebbe richiesto la soluzioni di circa 100000 problemi di programmazione lineare.

Quando presentò i progressi del suo progetto nel 1996, Hales affermò di essere in vista della fine, ma che avrebbe avuto ancora bisogno di "un anno o due". Nell'agosto del 1998 Hales annunciò che la dimostrazione era completa. A quell'epoca consisteva di 250 pagine di annotazioni e 3 gigabyte di programmi per computer, dati e risultati. Nonostante la natura inusuale della dimostrazione, gli editori degli Annals of Mathematics acconsentirono a pubblicarla, purché fosse accettata da una commissione di dodici referee. Nel 2003, dopo quattro anni di lavoro, il capo della commissione, Gábor Fejes Tóth (figlio di László Fejes Tóth), annunciò che la commissione era "certa al 99%" della correttezza della dimostrazione proposta da Hales, ma che non poteva garantire la correttezza di tutti i calcoli fatti al computer.

Nel febbraio del 2003 Hales pubblicò un articolo di cento pagine che descriveva nel dettaglio la parte non svolta al computer della sua dimostrazione. La rivista Annals of Mathematics sta continuando a pubblicare la parte teorica della dimostrazione di Hales. La parte computazionale verrà pubblicata in una diversa rivista, Discrete and Computational Geometry.

Una dimostrazione formale

Nel gennaio del 2003 Hales ha annunciato l'inizio di un progetto di collaborazione avente lo scopo di produrre una dimostrazione formale completa della congettura di Keplero. Lo scopo è quello di rimuovere qualsiasi incertezza residua sulla validità della dimostrazione creando una dimostrazione formale che può essere verificata da programmi di controllo automatico di dimostrazioni come HOL theorem prover. Questo progetto è chiamato Project FlysPecK, dove le lettere F, P e K sono le iniziali delle parole che compongono la frase Formal Proof of Kepler (dimostrazione formale di Keplero). Hales inizialmente stimò che sarebbero serviti circa 20 anni di lavoro per produrre una dimostrazione formale completa, mentre invece il progetto Flyspeck è terminato ufficialmente nell'agosto 2014.

Bibliografia

• (EN) G.G. Szpiro (2003) Kepler's Conjecture John Wiley & Sons ISBN 0471086010
• (EN) Thomas C. Hales (2003) A Proof of the Kepler Conjecture
• (EN) T. Aste and D. Weaire "The Pursuit of Perfect Packing" (Institute Of Physics Publishing London 2000) ISBN 0750306483

Collegamenti esterni

• (EN) Home page di Thomas Hales, su math.pitt.edu. URL consultato il 2 giugno 2006 (archiviato dall'url originale il 24 febbraio 2021).
• (EN) Descrizione della dimostrazione di Hales, su math.pitt.edu. URL consultato il 2 giugno 2006 (archiviato dall'url originale il 27 settembre 2011).
• (EN) Un articolo su NewScientist di Jacob Aron, su newscientist.com.
• (EN) Applicazione pratica della congettura di Keplero, su matifutbol.com.