Wallenberg Scholars

Datorer ska granska matematiska bevis

Matematikens abstraktioner når allt högre nivåer. Vissa bevis sträcker sig över tusentals sidor; de är så komplexa att ingen riktigt kan vara säker på att de är rätt. Därför tar nu matematiker datorer till hjälp. Thierry Coquand utvecklar datorprogram som ska kunna kontrollera bevis. Att visa att detta går, är i sig ett logiskt bevis; ett slags metamatematik.

Thierry Coquand arbetar normalt vid institutionen för data- och informationsteknik vid Göteborgs universitet. Men just nu tillbringar han ett år tillsammans med ett tjugotal andra matematiker och datorvetare på Institute for Advanced Study i Princeton, USA. De har ett gemensamt projekt: att försöka ta fram datorprogram som bevisar att matematiska bevis är korrekta.

– Det här är en unik möjlighet att få arbeta tillsammans med 20 andra personer som är intresserade av samma ämne som jag och som är väldigt duktiga, säger Thierry Coquand.

Långt bevis för hur en karta kan färgläggas

För att beskriva vikten av vad gruppen gör, ger han ett exempel: beviset för den så kallade fyrfärgssatsen. Den satsen säger att det krävs fyra olika färger för att kunna färglägga en karta, till exempel världskartan, på ett sådant vis att inga angränsande regioner, eller länder, har samma färg. Den här satsen framlades år 1852 och att bevisa den är inte lätt.

Det går att färglägga en karta på väldigt många olika vis och att undersöka alla kombinationer är ett gigantiskt arbete.
Hela fyra olika felaktiga bevis publicerades för satsen, innan en grupp matematiker år 1976 lyckades ta fram ett korrekt bevis med hjälp av ett datorprogram. Problemet var att beviset blev flera tusen sidor långt. Inom vetenskapen granskar alltid någon oberoende forskare resultaten från ett projekt innan de publiceras. Detta för att säkerställa att de resultat som går i tryck är korrekta och håller hög kvalitet. Men att granska detta långa bevis var i princip omöjligt.

– Beviset gick inte att överblicka. Dessutom använde de ett så icke-trivialt datorprogram, som sannolikt innehöll någon bugg, säger Thierry Coquand.
Detta ledde till en ny insikt inom matematiken: den började bli så komplicerad att matematiker inte längre kunde upptäcka varandras felaktigheter.

"Det som är bäst med Wallenberg Scholar anslaget, är att du är fri att göra vad du vill och att ta risker. Det är inte alls klart att det projekt jag arbetar med kommer att fungera. Men det är mycket bra att kunna utforska detta på ett så fritt sätt. Det är helt fantastiskt."

Risk för ett korthus som faller ihop

Därmed öppnade sig en ny obehaglig möjlighet: det fanns en risk att man började bygga ett korthus. Om någon detalj i grunden blev fel, kunde åratal av arbete falla ihop och tillintetgöras. Det långa beviset för fyrfärgssatsen, tillsammans med flera liknande exempel, blev därför startskottet för ett helt nytt forskningsområde, där datorvetare och matematiker utvecklar datorprogram som systematiskt kan gå igenom ett bevis.

Thierry Coquand har varit inblandad i utvecklingen av ett sådant system, som en annan forskare använde för att granska beviset för fyrfärgssatsen.

– Då hittade han till och med ett ännu bättre bevis, säger Thierry Coquand.

Han är med och organiserar året vid Princeton, där forskarna nu har samlats för att konstruera flera granskningsprogram för matematiska bevis. Initiativet till projektet tog den ryska matematikern Vladimir Voevodsky, professor vid Institute of Advanced Study och pristagare av det prestigefyllda Fields Medal, matematikens svar på Nobelpriset.

– Voevodsky menar att detta just nu är en av matematikens viktigaste utmaningar. Matematiker måste kunna lita på att tidigare arbeten är korrekta, säger Thierry Coquand.

Drömmen är att hitta det universella granskningsprogrammet

Själva forskningsområdet kallas för »type theory« och grundades av en svensk matematiker, Per Martin-Löf. Thierry Coquand berättar att Voevodsky för några år sedan kom på nya spännande tankar kring »type theory«; nya grundantaganden, så kallade axiom, som de kan bygga vidare på. Exakt vad det rör sig om är svårt att förstå för icke-matematiker.

– Men det här axiomet får väldigt spännande konsekvenser och jag arbetar med att förklara varför dessa nya principer är rättfärdigade.

Men hur kan forskarna då vara säkra på att de granskningsprogrammen i sig är korrekta och hittar alla fel?

– Det program som kontrollerar ett bevis är i sig ett kort program. Det går alltså att undersöka om programmet är korrekt genom en direkt genomgång, säger Thierry Coquand.

Även om det aldrig går att vara absolut säker på någonting, innebär detta en klar förbättring. När Thierry Coquand kommer hem till Sverige igen ska han fortsätta att utveckla dessa program. Han blev nyligen utsedd till Wallenberg Scholar. För den finansieringen som följer med utnämningen, tänker han försöka närma sig sina drömmars mål: att ta fram en programvara som kan granska alla matematiska bevis. Om detta är möjligt vet han ännu inte. Det är ett logiskt problem i sig; ett slags metamatematiskt problem.

Svaret ligger förmodligen långt in i framtiden. Under tiden ska han fokusera på delområden inom matematiken.

– För den matematik som användes för datoralgebra, skulle det kunna vara möjligt att ta fram ett bevisgranskningsprogram, säger han.

Lyckas forskarna kommer matematiken förändras i grunden. Då kan de matematiska bevisen bli ännu längre och abstraktionsnivån inom matematiken kan nå än högre höjder.

Text Ann Fernholm
Bild Magnus Bergström