Congettura di Keplero: problema finalmente risolto dopo 400 anni

Nel 1611, il fisico, matematico e astronomo tedesco Johannes Kepler propose che il modo migliore per impilare oggetti sferici - come i frutti, per esempio - sarebbe disporli sotto forma di piramide. Tuttavia, non riuscì a dimostrare di avere ragione, e questo enigmatico problema alla fine divenne noto come "congettura di Keplero".

Perché, secondo il New Scientist, nel 1998, il matematico americano Thomas Hales annunciò di essere stato in grado di dimostrare che la proposta di Keplero era corretta. All'epoca, Hales si basava su un metodo matematico per calcolare tutte le possibili possibilità di un teorema per arrivare alla soluzione.

Conti e più conti

Sulla base di questo metodo, Hales ha ritenuto che mentre esistono infiniti modi per impilare infinitamente oggetti sferici, la maggior parte di essi sono in realtà solo variazioni di alcune migliaia di possibilità. Così il matematico ha diviso il problema in migliaia di modi di organizzare oggetti sferici che rappresentavano matematicamente le infinite possibilità di disposizioni e ha gettato tutte queste informazioni nel software per fare i calcoli.

Il risultato è stato un piccolo stack di 300 pagine che ha richiesto quattro anni per essere controllato completamente da 12 revisori! E anche dopo tanto lavoro, i matematici non erano del tutto sicuri che i calcoli fossero corretti, sostenendo di essere sicuri solo del 99% che la soluzione di Hales sostenesse davvero la proposta di Keplero.

Finalmente sicuro al 100%

Bene, sai che "sicuro al 99%" non è abbastanza per la matematica, giusto? Nel 2003, Hales ha iniziato un progetto per provare i suoi calcoli, impiegando due software di verifica formale - Isabelle e HOL Light - per esaminare attentamente il suo lavoro.

E non è che alla fine siano arrivati ​​a una conclusione! Domenica scorsa, 10 agosto, il team di Hales ha annunciato che dopo aver tradotto la densa matematica presente sulle 300 pagine dei calcoli del 1998 in linguaggio computerizzato, sono stati in grado di stabilire che i calcoli sono corretti. In altre parole, dopo tanti secoli - e anni di sforzi da parte di Hales e del suo team - la proposta di Keplero è stata dimostrata.

E il fatto che lo spirito di Keplero possa finalmente riposare in pace - e Hales può rivolgere la sua attenzione a un altro problema complicato - non è l'unica buona notizia in tutta questa storia. Questa tecnologia può essere utilizzata per verificare l'enorme quantità di lavoro che arriva ogni anno, liberando i matematici da questo compito ingrato e permettendo loro di usare quel tempo per concentrarsi su altri problemi e liberare la loro creatività per esplorare l'universo dei numeri.