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, skriver kronikkforfatteren.(Illustrasjon: Shutterstock / NTB)
Kunstig intelligens revolusjonerer matematikken
KRONIKK: Ved hjelp av datamaskiner kan matematikkens beviser nå sjekkes grundigere og mer effektivt. Da er kanskje ikke veien lang til at datamaskinene også kan foreslå nye teoremer og bevise dem for oss.
HelgeHoldenProfessor ved Institutt for matematiske fag, NTNU
Publisert
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.
Kanskje man kan lære en maskin til å vite hva som er «interessant»? Og flere grupper rundt omkring i verden arbeider på dette.
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
Annonse
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?
Annonse
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.
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.
Annonse
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.
Annonse
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.
TA KONTAKT HER Har du en tilbakemelding på denne kronikken. Eller spørsmål, ros eller kritikk til Forskersonen/forskning.no? Eller tips om en viktig debatt?