Computertjek bekræfter den fuldstændige korrekthed af grønthandlerbeviset

‘Vi kan med glæde annoncere færdiggørelsen af ​​Flyspeck-projektet, der har givet et formelt bevis for Keplers formodning.’

Sådan blev det i søndags meddelt på Flyspeck-projektets hjemmeside.


Johannes Kepler formodede i 1611, at appelsiner pakkes tættest muligt på denne måde. Grønthandlere verden over gør det instinktivt. Thomas Hales beviste i 1998, at Keplers formodning var rigtig, men ingen anden matematiker kunne stå helt inde for Hales’ bevis. Nu har en computer eftervist, at Hales’ bevis er fuldstændigt korrekt. (Arkivfoto)

Meddelelsen er ikke nogen stor overraskelse, men den er banebrydende.

Den fjerner nemlig ikke kun en lille tvivl om et bevis fra 1998, men baner vejen for, at computere foruden at kunne bruges til at udarbejde matematiske beviser også kan bruges til at tjekke matematiske beviser – tilmed bedre end noget menneske er i stand til.

Tvivlen, der er nu er fjernet, drejer sig som nævnt om det bevis, som amerikaneren Thomas Hales i 1998 gav for Keplers formodning fra 1611 om, at den tætteste måde til at pakke appelsiner, kanonkugler eller andre sfæriske objekter er at lægge den i den velkendte grønthandlerstabel.

Ved denne form for pakning vil en andel på pi/sqrt(18)= 0,74048 af rumfanget være kugler, mens resten er luft.

Læs også: Efter 387 år kom stabelbeviset

300 sider og 187.000 linjer kode

Til trods for, at beviset lå færdigt i 1998, var det først i 2005, at Annals of Mathematics offentliggjorde det.

Det skete, efter at en gruppe matematikerne var kommet til enighed om, at beviset nok var mindst 99 pct. korrekt, men at de ikke kunne garantere for alle de computerberegninger, der indgik i beviset.


Dette billede fra 1998 viser Thomas Hales i færd med at pakke tennisbolde på den tætteste mulige måde. (Foto: University of Michigan).

Hales bevis var på 300 sider tekst og 187.000 linjer kode.

Det gik i store træk ud på at bevise formodningen ved en modstrid. Hales antog, at der fandtes en pakning af kuglerne, der havde en tæthed større end pi/sqrt(18) og viste, at dette førte til en modstrid. Derfor måtte den oprindelige antagelse være forkert.

Vejen til et formelt bevis

Allerede i 2003 satte Hales sig for sammen med flere af sine ph.d.-studerende og samarbejdspartnere at lave et formelt bevis, som ikke alene baserer sig på computerberegninger, men som også kan tjekkes med computerberegninger.

Det sidste er rent faktisk muligt med diverse matematiske hjælpeværktøjer.

Hales nye FPK-projekt (Formal Proof of Kepler conjuncture) skulle have et kort navn, hvor bogstaverne fpk kom i den rigtige rækkefølge. Valget faldt på ‘flyspeck’ eller fluelort på dansk.

Ved annonceringen af Flyspeck i 2003 var det Hales’ vurdering, at det kunne tage op til 20 år blive færdig.

Men efter at beviset nu er omskrevet til 300 sider ny tekst og kun 10.000 programlinjer, er det blevet tjekket med hjælpeværktøjerne HOL Light og Isabelle.

Opgaven har helt konkret bestået i at tjekke rigtigheden af mere end 23.000 uligheder.

Det har taget 5.000 processortimer eller omkring 156 timer i parallel på 32 kerner at nå frem til at eftervise rigtigheden af disse uligheder.

Chefprogrammøren for projektet, Alexey Solovyev fra University of Utah, gav i maj dette år en timelang beskrivelse af projektet under et besøg hos Microsoft. En beskrivelse, som der findes en videooptagelse af.

Fagfællebedømmelse kan være passé

Thomas Hales siger til New Scientist, at teknologien nu kan betyde et farvel til fagfællers vurdering i verifikationsprocessen (peer review).

‘Deres mening om korrektheden af et bevis har ikke længere nogen betydning,’ siger han.

Professor emeritus i matematik ved DTU Vagn Lundsgaard Hansen har tidligere over for Ingeniøren beskrevet processen med at acceptere et nyt omfattende matematisk bevis på denne måde.

»Kravet til et matematisk bevis er, at velmeriterede matematikere accepterer og anerkender beviset. Jo flere matematikere, der har mulighed for at sætte sig ind i beviset og kontrollere dets holdbarhed, jo bedre«.

Alan Bundy fra University of Edinburgh, UK, der ikke har været involveret i projektet, tilføjer, at han håber, at Flyspecks succes vil inspirere andre matematikere til at bruge hjælpeværktøjer til deres beviser.

»Dette eksempel kan blive normen i fremtiden,« siger han.

Posted in computer.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>