Kunstig intelligens revolu­sjonerer matematikken

Matematikk står overfor to store revolusjoner, og de skyldes datamaskiner. Ikke fordi de kan regne raskere og mer presist enn oss, som når vi benytter dem for å lage værmeldinger eller designe vindmøller. Men nettopp det som skiller matematikk – dronningen av vitenskapene – fra alle andre vitenskaper, nemlig bevisene. 

Datamaskinene kan nå sjekke at bevisene våre er riktige, slik at vi ikke er avhengige av at matematikere ikke gjør feil – det er den første revolusjonen. Da er kanskje ikke veien lang til at datamaskinene også kan foreslå nye teoremer og bevise dem for oss – det er den andre revolusjonen.

Vi kjenner alle Pytagoras’ læresetning fra skolen: Kvadraten på hypotenusen i en rettvinklet trekant er lik summen av kvadraten på de to katetene. Det gjelder for alle rettvinklede trekanter – store og små – i hele universet. 

Og vi vet at det er slik fordi vi har et matematisk bevis for dette, og dette har vært kjent i flere tusen år.

Hva er så et bevis?

Fra noen grunnleggende regler - såkalte aksiomer - for punkter og linjer og via logisk tenkning, kan vi i tilfellet over bevise at Pytagoras’ læresetning gjelder for absolutt alle rettvinklede trekanter. Ett bevis er nok. 

Bevisene kan forenkles og generaliseres, for eksempel til trekanter som ikke er rettvinklet, men riktigheten er bestemt av ett bevis. For trekanter som ikke nødvendigvis er rettvinklede kalles resultatet for cosinussetningen.

Matematikk og andre vitenskaper

Slik er det ikke i fysikk – vi trodde i flere hundre år at Newtons ligninger for gravitasjon ga den riktige beskrivelsen av bevegelsene til alle planeter i verdensrommet. 

Men så kom Einsteins relativitetsteori og endret dette radikalt, fordi Einsteins relativitetsteori for eksempel sier at intet kan bevege seg hurtigere enn lyshastigheten. I Newtons teori er det ingen øvre hastighet for bevegelse.

Inntil videre er det Einsteins ligninger som gir den beste beskrivelsen av gravitasjon. Innen medisin er man aldri fornøyd med én undersøkelse for å konkludere med en bestemt virkning. Innen andre vitenskaper er man kanskje aldri helt fornøyd. Og «sannhetene» endrer seg over tid i de fleste fag, men ikke i matematikk.

Men hvordan kan vi vite at et bevis er riktig? Bevisene blir lest av andre eksperter i feltet, og etter hvert danner det seg en enighet om at et bevis er riktig. Men eksperter kan ta feil, også i matematikk. Og bevisene blir lengre og lengre og dermed vanskeligere å forstå.

Beviset for klassifikasjonen av endelige, enkle grupper (det er ikke så farlig hva dette er, men man skal ikke la seg forlede av ordene «enkle» og «endelige») er på flere titusentalls sider, og gjennomført av over hundre matematikere over en periode på femti år.

Det betyr at beviset er for langt til at noen enkeltperson kan lese og forstå beviset.

Kan datamaskinene overta for matematikerne?

Flere grupper av matematikere har tenkt på om man kunne få datamaskiner til å sjekke bevisene og si at de helt sikkert er riktige. Da kan vi fjerne problemene med menneskelige feil, og altfor lange bevis. Men hvordan kan vi vite at dataprogrammene er riktige? 

I første omgang må dataprogrammene være bygget opp så enkelt at man kan stole på at iallfall de er korrekte. Videre må alle matematiske definisjoner og antagelser legges inn, helt fra de opprinnelige aksiomene slik at datamaskinen forstår «reglene».

Dette er en stor oppgave – matematikk har utviklet seg systematisk over en periode på over to tusen år. Deretter må man legge bevisene inn i datamaskinen. Det er en omfattende oppgave og krever at man både kjenner den matematiske teorien og hvordan dataprogrammet er konstruert.

Matematikere har startet å sjekke bevisene for de enkleste teoremene. Når disse er sjekket kan prøve å kontrollere de mer avanserte bevisene. Nå har man sjekket all matematikk opp til mastergradnivå, og – takk og pris – bevisene var alle riktige.

Men oppgaven med å sjekke beviset for et vanskelig teorem ble nylig satt på sin ultimate test så langt. Peter Scholze (f. 1987, tysk matematiker og Fields-medalje i 2018), en av verdens helt dominerende matematikere, var usikker på om beviset for et av hans mest avanserte resultater var riktig, og han utfordret bevis-sjekkerne til å verifisere beviset sitt.

Etter nær ett års hardt arbeid, hadde de lagt inn alle definisjoner og formalisert hans bevis. Så kunne man la maskinen sjekke beviset. Og svaret var at beviset var riktig. 

Dette var et stort stykke arbeid, fordi Scholzes resultat ligger helt i den fremste forskningsfronten. Men det viser også at det er ikke en enkel oppgave å sjekke riktigheten til et vilkårlig resultat.

Les hele artikkelen her: