Konsten att säkerställa korrekthet i datorprogram och matematiska bevis

Projektanslag 2020 Teknik/fysik/matematik

Att kontrollera att programvara i datorer verkligen räknar rätt är mycket svårt. Thierry Coquand leder ett projekt om system som hjälper till att kontrollera riktigheten i matematiska resonemang, så kallade interaktiva bevissystem.

Projektanslag 2020

Projekt:
”Type Theory for Mathematics and Computer Science”

Huvudsökande:
Professor Thierry Coquand
Göteborgs universitet

Medsökande:
Stockholms universitet
Peter LeFanu Lumsdaine

Beviljat anslag:
34 700 000 kronor under fem år

− 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 Thierry Coquand, professor i datavetenskap vid Göteborgs universitet.

Metoden har använts med framgång när det gäller att kontrollera programvara som används i till exempel flygelektronik.  

Bra metod också för korrekthet i komplexa matematiska bevis

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 
Bild  Camilla K. Elmar / Senter for grunnforskning.