KI har gått fra ord til bevis. Hva betyr det for oss? Foto: PrivatFremfor alt trenger vi fagmiljøer som uavhengig kan etterprøve selskapenes påstander.Publisert: 12.08.2026 20:00Ett av OpenAIs nye bevis er lengre enn en roman: over 37.000 linjer med datakontrollert kode. Det hevder å velte en mer enn 40 år gammel antakelse fremsatt av Alain Connes. Han har vunnet Fields-medaljen, matematikkens kanskje mest prestisjefylte pris, og er særlig kjent for arbeid innen operatoralgebraer.Grovt sagt spurte Connes om et bestemt matematisk «fingeravtrykk» alltid røper objektet det kommer fra. Astra hevder å ha funnet ulike objekter med samme avtrykk.Få dager senere ble det hevdet i sosiale medier at KI-en hadde gjennomført logikken riktig, men løst feil problem. Den konkrete innvendingen ser, så langt vi kan vurdere, selv ut til å bygge på en matematisk sammenblanding. Foto: OpenAIMatematikeren Shuoxing Zhou la samtidig frem et annet moteksempel til Connes’ antakelse, også funnet med KI-hjelp. Det avgjør ikke om OpenAIs arbeid er riktig. Saken viser likevel hvor raskt både mulige gjennombrudd og påstander om fatale feil sprer seg.Et gjennombrudd – med forbeholdConnes-arbeidet er ett av ti manuskripter OpenAI offentliggjorde nylig. De spenner fra kulepakking i høye dimensjoner til et abstrakt objekt ingen visste fantes. Til sammen fyller de 249 sider.Ifølge OpenAI fant modellen Astra løsningene. Astra er navnet OpenAI bruker på KI-systemet som hjalp til med å finne og bearbeide bevisene. Mennesker bearbeidet manuskriptene med modellen, før argumentene ble formalisert i Lean,Lean,https://snl.no/lean som kontrollerer matematiske slutninger trinn for trinn.OpenAI anslår at bruken av modellen for å finne løsningene ville ha kostet rundt 2000 dollar. Det omfatter ikke utvikling og trening. Når modellen først finnes, er det likevel billig å produsere nye beviskandidater.Vi mener dette er et gjennombrudd på grunn av bredden, selv om hvert resultat ennå ikke er sikkert. Ett overraskende treff kunne vært flaks. Ti resultater fra ulike områder er vanskeligere å overse.Men ti manuskripter er ikke ti aksepterte teoremerteoremerhttps://snl.no/teorem. Lean kan kontrollere at en påstand følger av bestemte definisjoner. Systemet avgjør ikke om påstanden svarer til det historiske problemet, om resultatet er nytt, eller hvilken betydning det har. Det må fagfolk vurdere.Fra språkmodell til forskningsverktøyDe færreste har noen grunn til å bry seg om Connes’ formodning i seg selv. Det interessante er hva saken forteller om KI-utviklingen.Grunnteknologien ble utviklet for å forutsi og generere språk, ikke for matematisk forskning. Likevel brukes systemer som springer ut av denne teknologien nå til problemer de ikke opprinnelig ble laget for.Matematikken gjør endringen særlig tydelig, fordi et argument kan kontrolleres trinn for trinn. På andre områder er det ofte langt vanskeligere å vite om et svar faktisk er godt.Hva endres i den matematiske hverdagen?Vår kollega, professor Fabian Harang ved Handelshøyskolen BI og SURE-AI, lot en språkmodell gjennomgå et manuskript kritisk. Den fant reelle svakheter og hjalp med kode som testet metoden. Et arbeid som før ville tatt uker, ble gjort på dager – men alt måtte kontrolleres.Det stemmer med våre erfaringer. Modellene kan hjelpe med litteratursøk, kode og jakt på svake punkter. Men de kan også vise til artikler som ikke finnes eller levere elegante argumenter med et avgjørende hull.Førsteamanuensis Cris Salvi ved Logos Research og Imperial College London peker på flaskehalsen: Det er blitt billig å produsere matematikk som ser overbevisende ut. Grundig kontroll kan ikke fremskyndes like mye. Derfor kan ikke kravene til dokumentasjon og ansvar senkes.Også undervisningen må endresStudenter kan allerede få overbevisende løsninger på mange oppgaver på sekunder. Hvis et skriftlig svar er det eneste beviset på læring, tester vi snart tilgangen til KI-verktøy mer enn matematisk forståelse.Et generelt forbud er ikke svaret. Universitetslektor Jan-Fredrik Olson ved Lunds universitet og Universitetet i Oslo, som vi har rådført oss med, påpeker at det kan frata studentene veiledet erfaring med en teknologi de senere skal bruke.Når bevisene blir billige, blir dømmekraften dyrbarVi trenger eksamener der studentene må forsvare løsninger muntlig, finne feil i KI-genererte argumenter og sammenligne forslag. Den som skal kontrollere maskinens arbeid, trenger fortsatt et solid matematisk fundament.Vi tror ikke dette gjør matematikere overflødige. Men arbeidet deres vil endre seg. Det kan bli brukt mindre tid på å finne det første forslaget og mer tid på å kontrollere forutsetningene, forstå betydningen og avgjøre hvilke spørsmål som faktisk er verdt å undersøke.En oppgave for universiteteneUniversitetene bør bygge kompetanse i KI-støttet matematikk og formelle metoder. Tidsskrifter og institusjoner må avklare hvordan KI-bruk skal dokumenteres. Fremfor alt trenger vi fagmiljøer som kan etterprøve selskapenes påstander uavhengig.OpenAI fortjener anerkjennelse for å ha lagt frem manuskripter og formelle sertifikater som gjør seriøs etterprøving mulig. Likevel utvikler det samme selskapet modellen, velger problemene og forklarer hva resultatene betyr. Fagmiljøet kan ikke nøye seg med å være publikum.Connes-episoden viser at også vi kan gripe for raskt etter en enkel fortelling. Hverken et Lean-sertifikat eller et innlegg som sprer seg i sosiale medier, kan alene avgjøre om problemstillingen er riktig, om resultatet er nytt eller hvilken betydning det har.Det er allerede mulig å produsere flere matematiske forslag enn fagmiljøet rekker å kontrollere. Universitetenes oppgave blir derfor ganske konkret: De må utdanne mennesker som kan skille gjennombrudd fra blindspor og spørre: Har vi faktisk bevist det vi tror vi har bevist?Når bevisene blir billige, blir dømmekraften dyrebar.