Keplers formodning: problemet ble endelig løst etter 400 år

I 1611 foreslo den tyske fysikeren, matematikeren og astronomen Johannes Kepler at den beste måten å stable sfæriske gjenstander - som for eksempel frukt - ville være å arrangere dem i form av en pyramide. Imidlertid kunne han ikke bevise at han hadde rett, og dette gåtefulle problemet ble etter hvert kjent som "Kepler Conjecture."

For ifølge New Scientist i 1998 kunngjorde den amerikanske matematikeren Thomas Hales at han hadde klart å bevise at Keplers forslag var riktig. På den tiden stolte Hales på en matematisk metode for å beregne alle mulige muligheter for et teorem for å komme frem til løsningen.

Kontoer og flere kontoer

Basert på denne metoden vurderte Hales at selv om det er uendelige måter å stable sfæriske objekter uendelig, er de fleste av dem bare varianter av noen få tusen muligheter. Dermed delte matematikeren problemet i tusenvis av måter å organisere sfæriske objekter som matematisk representerte de uendelige mulighetene for ordninger, og kastet all denne informasjonen inn i programvare for å gjøre beregningene.

Resultatet var en liten stabel på 300 sider som tok fire år å fullstendig sjekke av 12 anmeldere! Og selv etter så mye arbeid, var matematikere ikke helt sikre på at beregningene var riktige, og hevdet at de bare var 99 prosent sikre på at Hales løsning virkelig støttet Keplers forslag.

Endelig 100% sikker

Vel, du vet at "99% sikker" ikke er nok til matematikk, ikke sant? For i 2003 startet Hales et prosjekt for å bevise beregningene sine, ved å bruke to formelle verifiseringsprogrammer - kalt Isabelle og HOL Light - for å granske arbeidet hans.

Og det er ikke slik at de endelig kom til en konklusjon! Forrige søndag 10. august kunngjorde Hales team at etter å ha oversatt den tette matematikken som var til stede på 300 sider i 1998-beregningene til datastyrt språk, kunne de konstatere at beregningene stemmer. Med andre ord, etter så mange århundrer - og år med innsats fra Hales og hans team - er Keplers forslag blitt bevist.

Og at Keplers ånd endelig kan hvile i fred - og Hales kan rette oppmerksomheten mot et annet komplisert problem - er ikke den eneste gode nyheten i hele denne historien. Denne teknologien kan brukes til å sjekke den enorme mengden arbeid som dukker opp hvert år, og frigjøre matematikere fra denne takknemlige oppgaven og la dem bruke den tiden til å fokusere på andre problemer og slippe løs kreativiteten til å utforske tallenes univers.