Nya verktyg för felsökare

Dr Anders Mörtberg får anslag från Knut och Alice Wallenbergs Stiftelse, till en postdoktoral tjänst för att rekrytera en forskare från utlandet till Matematiska institutionen vid Stockholms universitet.

När moderna datorprogram och matematiska teorier blir alltmer komplexa blir det också allt svårare att vara säker på att de är helt fria från buggar och misstag. En metod för att öka tillförlitligheten är att använda en bevisassistent – ett datorprogram som kan verifiera att koden är buggfri. Målet för projektet är att utveckla de teorier som ligger till grund för moderna bevisassistenter.

Bevisassistenter kan även användas för att verifiera komplicerade matematiska bevis. Ett exempel är fyrfärgssatsen som säger att alla planära kartor kan färgläggas med endast fyra färger så att inga närliggande länder har samma färg. Satsen bevisades 1976 med hjälp av över 1 000 timmar långa datorberäkningar vilka i sin tur behövde granskas. En formell bekräftelse kom slutligen 2005 då en bevisassistent kunde visa att beräkningarna var fria från buggar. 

Många av dagens bevisassistenter bygger på typteorier, en samling logiska system utvecklade med målet att utgöra grunden för all matematik. Den första moderna typteorin konstruerades på 1970-talet av Per Martin-Löf, professor emeritus i logik vid Stockholms universitet. Under de senaste åren har utvecklingen av typteorin inspirerats av dess kopplingar till homotopiteori, en del av det matematiska fältet algebraisk topologi. Ur en förening mellan de två teorierna har ett antal nya idéer, axiom och metoder vuxit fram för att tackla frågor om verifiering. Syftet med projektet är att förutom arbetet med teoretiska modeller även vidareutveckla redan kända bevisassistenter så att buggar i matematiska bevis och program bättre kan förebyggas.

Foto: Kristoffer Sahlin