La questione non è di poco conto come potrebbe sembrare, perché da certezze scientifiche apparentemente banali discendono conseguenze importanti. In questo caso, ad esempio, ma migliore organizzazione e ottimizzazione dei dati in un computer. Ma basterebbe pensare all’orgoglio rinvigorito dei fruttivendoli e alle ricadute possibili che ciò può avere sui consumi di frutta e verdura e sul Pil nazionale, per apprezzare quanto è riuscito a fare Thomas Hales della University of Pittsburgh, in Pennsylvania.
Il matematico americano ha risolto la congettura di Keplero che da 400 anni non aveva raggiunto il 100% nei livelli di dimostrazione. Quale forma geometrica, si era chiesto l’astronomo polacco, è la più adatta per impilare nel modo migliore oggetti sferici, come per esempio le arance?
Nel 1611 Keplero ipotizzò che la forma fosse quella usata nei negozi di frutta, ovvero la piramide. Il problema dell’impacchettamento più denso delle sfere divenne così importante da diventare il diciottesimo dei ventitré problemi con cui Hilbert, nel 1900, sfidò i matematici di tutto il mondo all’alba del nuovo secolo.
Thomas Hales ha ora finalmente dimostrato quella congettura empirica, risolvendo un problema che arrovella i matematici, a guardarci bene, ancora prima di Keplero: dalla fine del XVI secolo, quando Sir Walter Reigh si mise alla ricerca di una formula rapida per calcolare il numero di palle di cannone contenute in un cumulo.
La piramide minimizza gli spazi tra le sfere con un’efficienza del 74 per cento, ossia del 22 per cento in più, per esempio, della struttura cubica. Un impacchettamento che parta da una base di sfere disposte a griglia esagonale si avvicina, ma non eguaglia la piramide. Lo hanno dimostrato al termine di 16 anni di studi, i due software Isabelle e HOL Light, a cui spettava individuare eventuali errori compiuti nelle catene di passaggi logici.
Hales ha combattuto con questo problema dal 1998, quando presentò il primo attacco alla congettura valutando, tramite un software, alcune migliaia di disposizioni delle sfere che da sole rappresentavano le infinite combinazioni possibili. Un lavoro di 300 pagine che impegnò dodici revisori per quattro anni. Anche dopo la pubblicazione sulla rivista Annals of Mathematics nel 2005, i revisori non andarono oltre un “è corretta al 99 per cento”. Nel 2003, Hales aveva intanto avviato il progetto Flyspeck, per arrivare a una completa verifica formale della sua dimostrazione.
Ora non è più necessaria la verifica umana: la dimostrazione di Hales è corretta e la congettura di Keplero era giusta. I fruttivendoli possono continuare a impilare mele e arance come hanno fatto sempre e noi ringraziamo Hales per non averci tolto, in questa epoca di incertezze, almeno questa convinzione.
(20 agosto 2014. Fonte: Wired)
