Forskersonen er forskning.nos side for debatt og forskernes egne tekster. Meninger i tekstene gir uttrykk for skribentenes holdninger. Hvis du ønsker å delta i debatten, kan du lese hvordan her.

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.

les også:

Newton og Einstein sine teoriar feilar nærast overalt

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.

Hvor mange farver trengs for å farvelegge et kart?

Et enklere eksempel er dette: Hvor mange farver trenger man for å farvelegge et kart slik at to naboland ikke får samme farve? Spørsmålet ble stilt i England på midten av 1800-tallet i forbindelse med farvelegging av «counties» i England. Ved prøving og feiling fant man fort ut at 3 farver var for lite, men ingenklarte å finne et kart som krevde mer enn 4 farver.

I 1852 påstod matematikere at 4 farver var tilstrekkelig, og de første «bevisene» kom raskt deretter. Men det tok mer enn 10 år før man fant ut at «bevisene» ikke var korrekte. Og først i 1976 ble det såkalte firfarveteoremet bevist av amerikaneren Kenneth Appel og tysk-amerikaneren Wolfgang Haken – 4 farver er tilstrekkelig for alle kart.

Det fins jo uendelig mange forskjellige kart, men Appels og Hakens store prestasjon var å bevise at det var nok å sjekke et endelig antall kart. Her er det en stor forskjell på «uendelig» og «endelig». 

Om du skal kontrollere uendelig mange kart, trenger du uendelig med tid. Med et endelig antall tilfeller, trenger du i prinsippet bare lang nok tid. Imidlertid var antallet altfor stort til å kunne sjekkes for hånd.

Dermed måtte Appel og Haken skrive et dataprogram for å sjekke riktigheten. Dette skiller seg fra beviset til Scholze der vi har et bevis som er vanskelig, men som kan sjekkes av matematikere.

Trenger vi (menneskelige) matematikere?

Men det er én hake ved det jeg har forklart så langt – datamaskinen kan bare kontrollere et bevis som allerede er laget av (menneskelige) matematikere. Det betyr at matematikerne fortsatt er i førersetet. Dette har ikke noe med kunstig intelligens å gjøre.

Men kan man lage maskiner som også foreslår teoremene og lager bevisene selv? Det er den andre revolusjonen, og her kommer kunstig intelligens inn.

Datamaskiner er gode til å se mønstre, og om all matematisk kunnskap er lagret i datamaskinene, så kan maskinene foreslå nye teoremer, og kanskje også lage bevis for disse. Det er iallfall lett å tenke seg at dette kan skje. Men problemene fremover for å komme dit er formidable.

Videre er noe annet som er lett å undervurdere – nemlig er de nye teoremene «interessante»? Det første kriteriet er selvsagt om beviset er riktig. Men så er det spørsmålet om det et uventet resultat eller om beviset er originalt eller vanskelig – det er det som avgjør om kunstig intelligens kan hjelpe matematikken.

Kanskje man kan lære en maskin til å vite hva som er «interessant»? Og flere grupper rundt omkring i verden arbeider på dette.

Man skal være forsiktig med å si at noe er umulig om det ikke strider mot fysikkens naturlover. Men det er vanskelig å tenke seg at en datamaskin kan komme med de virkelige disruptive nyskapningene – for eksempel matematisk gruppeteori som er en nødvendighet for å oppnå sikker kommunikasjon på internett, den nye geometrien som var en forutsetning for relativitetsteorien, eller å skape musikken til The Beatles. Det er vår trøst og vårt håp.

Les også:

Dette kan redusere kronisk hodepine

Falsk forskning truer demokratiet