AI har börjat bevisa matematik. Vem kontrollerar att det stämmer?

Den 6 oktober hände något som matematiker kommer att prata om länge. På en enda dag lade OpenAI ut 722 manuskript på GitHub, med påståenden om framsteg på 372 öppna problem. Dagen efter drogs tre av dem tillbaka. Det är lätt att se det som en nyhet om matematik. Jag tycker att det är något större: ett test på hur vi hanterar AI som kan producera kunskap snabbare än vi kan granska den.

Vad hände egentligen?

Manuskripten kommer från en intern OpenAI-modell som inte är tillgänglig för någon utomstående. Tre av dem drogs tillbaka den 7 oktober sedan ett teckenfel gjort ett argument ogiltigt i ett manuskript och konstruktionen i två andra som byggde på det. Ytterligare 14 har reviderats, enligt Retraction Watch. OpenAI säger själva att processen är iterativ och att de välkomnar granskning.

Bara 42 procent av resultaten är kodade i Lean, ett språk där en dator kontrollerar varje logiskt steg, skriver Scientific American. Resten har ingen maskinell kontroll, och kvaliteten är mycket ojämn. Roland Bauerschmidt vid New York University säger att han skulle ha raderat vissa av texterna om de kommit från en främling.

Samtidigt innehåller högen något som får erfarna matematiker att ta sig för pannan på andra sätt. Det gäller beviset för den så kallade kvasi-Riemannhypotesen.

Det som får experterna att tystna

Riemannhypotesen har stått olöst i över 160 år och kallas av Quanta Magazine för kanske matematikens största öppna fråga. Kvasi-versionen är svagare, men ändå mycket kraftfull: den säger att alla icke-triviala nollställen ligger i en smalare remsa än man tidigare kunnat visa. Ju smalare remsa, desto mer vet vi om hur primtalen är fördelade.

OpenAI presenterade två versioner. Den ena, på 199 sidor, är verifierad i Lean. Den andra, på 49 sidor och med en snävare gräns, är inte maskinverifierad, men det är den matematikerna nu studerar. Enligt Quanta är den dessutom det enda av de 722 manuskripten som en människa har redigerat. Experterna är i stort sett överens om att resultatet verkar stämma. Jared Duker Lichtman vid Stanford kallar det det viktigaste AI-resultatet inom matematik hittills, med god marginal.

Och ändå: Maksym Radziwiłł vid NYU kallar båda texterna fruktansvärt dåligt skrivna, och menar att en tidskrift skulle ha refuserat dem direkt. Peter Sarnak vid Princeton har lagt om en kurs för att studera beviset, men vill inte kalla det för en sats förrän människor har kontrollerat och förstått varje detalj. Och Will Sawin, också han vid Princeton, tror att den fulla Riemannhypotesen fortfarande ligger långt bort.

Det var inte första gången i år. I maj meddelade OpenAI att en intern modell motbevisat en gissning av Paul Erdős från 1946. I juli presenterade Levent Alpöge vid Anthropic ett motexempel till Jacobiangissningen, framtaget med hjälp av Claude och kontrollerat i bevisverktyget Isabelle/HOL. Motexempel är enkla att granska. Långa bevis är det inte.

Därför är matematikerna oroade

Den 11 september skrev 25 Fields-medaljörer under ett upprop, A Severe Misalignment of AI in Mathematics, som Terence Tao publicerade på sin blogg. Bland undertecknarna finns Peter Scholze, Cédric Villani och Maryna Viazovska. Deras poäng är inte att AI ska förbjudas. De skriver tvärtom att tekniken kan fördjupa och påskynda matematiskt arbete. Men de menar att AI-bolagens mål och matematikens mål är allvarligt osynkade.

Problemet, enligt dem, är att berömda problem har blivit mätstockar. Att lösa ett problem är ett verktyg, inte målet. Målet är förståelse. När lösningar presenteras i all hast, utan genomgång av metoderna och utan ordentlig hänvisning till tidigare arbete, uppstår frågor om vem som egentligen ska ha äran. Och en strid ström av sanna och falska resultat kan, som de uttrycker det, förstöra den bördiga jorden i stället för att ge liv åt nya idéer.

Samma tema återkommer i reaktionerna på OpenAIs släpp. Association for Human Mathematics kallade massutgivningen en maktdemonstration snarare än ett vetenskapligt bidrag, och uppmanade matematiker att sluta arbeta med OpenAI. Andrew Sutherland vid MIT vill att bolaget också redovisar alla problem modellen misslyckades med, tusentals enligt OpenAI. Flera matematiker misstänker dessutom att modellen själv har valt problemen. Det har OpenAI inte svarat på.

Motargumenten är värda att ta på allvar

Det finns en annan sida, och den är inte dum. Harvardmatematikern Michael Douglas menar att vi står vid början på en ny epok. Hector Pasten i Chile lyfter fram att OpenAI faktiskt har blivit bättre på att ge kredit. Och OpenAI hävdar att deras rådgivargrupp av matematiker rekommenderade att släppa resultaten utan att vänta på full formalisering. Bolaget säger också att de rättar fel och drar tillbaka papper som inte går att laga.

Det är dessutom svårt att argumentera mot det enklaste svaret: om ett bevis är rätt, spelar det då roll vem eller vad som hittade det? Matematiken har alltid avgjorts av granskning, inte av vem som skrev först.

Men det är här jag tycker att argumentet brister. Granskning är en knapp resurs. Skillnaden mellan att visa en lösning och att få den förstådd kan vara år av mänskligt arbete. Och när några få bolag bestämmer takten, valet av problem och tidpunkten för offentliggörandet, är det inte längre ett samarbete mellan människa och maskin. Det är en maktfråga.

Fyra krav jag tycker att vi bör ställa

Verifiera först, annonsera sedan. Alex Townsend vid Cornell har föreslagit att OpenAI borde ha släppt de Lean-verifierade resultaten först, och de övriga i en separat omgång. Det är ett rimligt minimikrav.

Redovisa misslyckandena. Ett resultat betyder mer när vi vet hur många försök som ligger bakom det. Utan det går det inte att bedöma hur imponerande något är.

Var tydlig med ursprung och kredit. Vem valde problemet, vilka människor byggde resultatet på, och vem har gått igenom texten? Det är frågor som en forskare måste kunna få svar på.

Sikta på förståelse, inte bara svar. Terence Tao visar en väg i ett experiment där AI används för att öka människors förståelse snarare än ersätta den, med öppen redovisning och gemensamt arbete, ungefär som ett Polymath-projekt för AI-eran.

Det här är Human in the Loop på riktigt

Det som händer i matematiken är en förhandsvisning av något som kommer att hända överallt. När AI kan producera mer än vi hinner läsa blir Human in the Loop ingen slogan utan en praktisk nödvändighet: någon måste förstå, granska och stå för det som sägs. Det hänger ihop med hur vi mäter AI, som jag skrev om i artikeln om evals, och med frågan om hur nära AGI egentligen är.

Har AI blivit bättre än matematikerna? Kanske inte än. Men frågan är inte längre om maskinerna kan bidra. Frågan är vilka spelregler vi kräver innan vi låter dem avgöra vad som är sant.