Skip to main content
DA / EN

Endelig færdig med 10 milliarder års matematisk hjernegymnastik

Hvis der ikke fandtes computere, ville denne opgave kræve 10 milliarder år af en matematikers vågne tid. Men der står heldigvis en supercomputer på SDU, og derfor er opgaven nu løst. Resultatet har betydning for vores tillid til alle de store og små elektroniske maskiner, der styrer vores hverdag.

Af Birgitte Svennevig

Sidste år meddelte et stolt forskerhold fra University of Texas i Austin, at det var lykkedes at løse et matematisk problem, der har spøgt i miljøet i mere end 30 år.

Forskerne havde sat supercomputeren Stampede fra Texas Advanced Computing Centre på opgaven – men da computeren havde spyttet sit svar ud, stod de med et nyt problem: De kunne ikke tjekke det fremkomne bevis matematisk. Det var simpelthen for stort. Og eftersom næsten alle computerprogrammer indeholder fejl i større eller mindre grad – det har vi alle oplevet i vores hverdag – ville det være for usikkert at stole på Stampede’s beregning.

Derfor efterlyste Texas-forskerne med det samme en matematisk verificering af det fremkomne matematiske bevis (som i parentes bemærket fylder 200 terabytes data, svarende til at skulle læse ca. 1800 millioner e-bøger).

- Det er det største matematiske bevis nogensinde, og at verificere så stort et bevis kræver en ekstremt stor indsats. Det ville kræve 10 milliarder års koncentreret læsning at gå det igennem for at se efter eventuelle fejl, forklarer Peter Schneider-Kamp, professor mso, Institut for Matematik og Datalogi, SDU.

Ned i tid, tak

Sammen med kollegerne postdoc Luís Cruz-Filipe fra Institut for Matematik og Datalogi på SDU og professor Joao Marques-Silva fra universitetet i Lissabon satte han sig for at gøre et forsøg alligevel – med hjælp fra supercomputeren ABACUS, der står på SDU. Deres resultater er tilgængelige her.

- Vi oplærte ABACUS til at være en kunstig matematiker med meget høj kapacitet, så vi kunne komme ned på et par dages arbejdstid i stedet for 10 milliarder år.

Forskerne har IKKE lavet en genberegning, men har i stedet skabt et program, der er såkaldt "correct by construction", eftersom det er lavet ud fra en formalisering af den matematiske teori bag beviset.

- Det er derfor garanteret, at vores program ikke tager fejl. Og da det har gennemgået alle 200 TB af beviset, er det også garanteret, at texanernes bevis er matematisk set korrekt.

Det bliver nemmere at skabe tryghed omkring computere

Med andre ord: Texanernes bud på en løsning af det matematiske problem er rigtig nok.

- Det er fantastisk, at Luis, Peter og Joao er lykkedes med at verificere det største matematiske problem nogensinde. Deres arbejde bidrager væsentligt til, at vi nu kan have tillid til rigtigheden af vores resultat, siger Marijn Heule fra University of Texas, der var med til at løse det matematiske problem.

- Det væsentlige er dog ikke så meget, at vi har bekræftet nogle andre forskeres resultat. Det vigtige her er, at vi har vist, at computerberegninger kan verificeres matematisk, og det kan vi bruge til at styrke vores tillid til alle de store og små computere, der styrer vores hverdag. Når vi matematisk kan bevise, om et hard- eller softwaresystem fungerer korrekt, kan vi have større tillid til det pågældende stykke hard- eller software. Og det synes jeg personligt er meget betryggende, hvis jeg f. eks. skal sætte mig ind i en selvkørende bil eller et fly, der styres af software, siger Peter Schneider-Kamp.

Styrker tilliden til hverdagens computere

Vores hverdag er fyldt med computere, og det er vigtigt, at vi kan stole på, at de fungerer sikkert. De sørger eksempelvis for at sende brændstof til vores bilers motor, at vi kan sende mails, at vi kan hæve penge, at apoteket udleverer den rigtige medicin, at fly holder den rigtige højde, at lægen kan stille den rigtige diagnose, osv. Iflg. professor Peter Schneider-Kamp kan det nye arbejde bidrage til at styrke tilliden til dem.

Forskerkontakt

Professor mso Peter Schneider-Kamp, Institut for Matematik og Datalogi. email: petersk@imada.sdu.dk. Telefon 6550 2327.

Gå til profil

Redaktionen afsluttet: