Endelig færdig med 10 milliarder års matematisk hjernegymnastik

Af Birgitte Svennevig, birs@sdu.dk, 10-11-2016

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å Stampedes 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, der er professor på Institut for Matematik og Datalogi.

Ned i tid, tak

Sammen med SDU-kollegaen postdoc Luís Cruz-Filipe 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 terabytes af beviset, er det også garanteret, at texanernes bevis er matematisk set korrekt.

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 selv 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.