400 år gammel gåte løst
Oppgaven ble for stor for mennesker.
Året er 1611 og vitenskapsmannen og matematikeren Johannes Kepler har fundert lenge og vel på et hverdagslig problem. Hva er den mest effektive måten å stable kuler på? Vi kan forestille oss kjøpmenn med epler og appelsiner i bodene sine som ivrig ventet på svar.
Og Kepler var overbevist om at han hadde svaret: I pyramideform. Problemet var bare at han ikke klarte å bevise det matematisk.
Vitenskapen har siden diskutert problemet i det vide og brede, men ingen har klart å verifisere at pyramidestabling er mest effektivt. Eller, det vil si, i 1998 regnet matematikeren Thomas Hales seg frem til et bevis, men det tok tolv uavhengige matematikere fire år å dobbelsjekke den 300 sider lange bevisutregningen. Og de var fremdeles ikke hundre prosent sikre på at det stemte.
Men nå har Hales utviklet et dataprogram kalt "Flyspeck" som etter alt å dømme verifiserer utregningene hans, skriver New Scientist.
Prosjektet bruker to vanlig brukte dataverifiseringsverktøy kalt "Isabelle" og "HOL Light" som begge kan benyttes til å verifisere mindre, logiske påstander. Med nok tid kan de brukes til å verifisere matematiske bevis del for del.
Og endelig, søndag 10. august, annonserte Hales forskningsgruppe at hans 300 sider lange utredning var gjennomgransket av dataverktøyet, og at alt stemte.
En datamaskin har med andre ord endelig verifisert en 400 år gammel idé lagt frem av Johannes Kepler.
- Jeg følte meg med ett ti år yngre, sier Hales til New Scientist.
Prosjektet har samtidig en annen konsekvens, skriver bloggen Gizmodo. Det legges frem hundrevis av matematiske bevis hvert år, og "Flyspeck" demonstrerer at de kan gås etter i sømmene av datamaskiner istedenfor av mennesker - som betyr at matematikere isteden kan bruke tiden sin kreativt til finne ut hvordan matematikken kan anvendes.