35 miljoner kronor från KAW till forskning om interaktiva bevissystem
Att kontrollera att programvara i datorer räknar rätt är mycket svårt. Thierry Coquand, professor i datavetenskap vid Göteborgs universitet, får 35 miljoner kronor av Knut och Alice Wallenbergs Stiftelse för ett projekt om system som hjälper till att kontrollera riktigheten i matematiska resonemang, så kallade interaktiva bevissystem.
− Knepet är att använda programvara för att verifiera programvara. Grundidén är att betrakta program, deras indata och utdata, som matematiska objekt och ställa en matematisk exakt fråga om deras korrekthet, säger professor Thierry Coquand.
Metoden har använts med framgång när det gäller att kontrollera programvara som används i till exempel flygelektronik.
Enligt Thierry Coquand börjar behovet av den här typen av beviskontroll även märkas i ren matematik. Anledningen är att längden och komplexiteten har ökat hos matematiska bevis.
− Två exempel är Feit-Thompsons sats på mer än 250 sidor och fyrfärgssatsen, vars bevis var omöjligt att genomföra för hand. Båda bevisen har nu kontrollerats av interaktiva bevissystem.
Thierry Coquands projekt tar avstamp i teorier formulerade av den rysk-amerikanska matematikern Vladimir Voevodsky. För ett decennium sedan blev han alltmer bekymrad över komplexiteten hos bevis i sin egen forskning.
− Hans nya sätt att se på matematiska objekt har banbrytande konsekvenser för matematikens grundvalar, och i utformandet av interaktiva bevissystem, säger Thierry Coquand.
Text: Thomas Melin
Projektet ”Type Theory for Mathematics and Computer Science” får 34 700 000 kronor och löper under fem år. Det kommer att vara ett samarbetsprojekt mellan datalogen Thierry Coquand och matematikern Peter Lumsdaine vid Stockholms universitet.
Sammanlagt har 18 forskningsprojekt beviljats totalt 541 miljoner kronor av Knut och Alice Wallenbergs Stiftelse.