DeepMinds nio bevis prövas för nyhetsvärde

Ett matematiskt bevis kan vara elegant och ändå dölja en lucka som ingen upptäcker på flera år. Googles AI-agent AlphaProof Nexus tog fram bevis för nio problem som Paul Erdős hade ställt, och programvara kontrollerade varje steg. Arbetet publicerades först som ett förhandsmanus i maj (arXiv) och därefter, efter sakkunniggranskning, i Science den 8 oktober (Science). Programvaran kunde bekräfta att bevisen höll, men om de tillförde något nytt fick matematiker avgöra.

En granskare som inte låter sig charmas

Chattbotar kan formulera matematik som låter övertygande. En självsäker text kan dölja ett saknat steg som bara en noggrann läsare upptäcker. AlphaProof Nexus undviker den fallgropen genom att arbeta i Lean, ett programmeringsspråk där definitioner, påståenden och bevis formuleras så exakt att en dator kan kontrollera dem.

Tänk på Lean som en granskare som går igenom varje rad i ett färdigt bevis och tillämpar fasta regler. Stil ger inga poäng. Om ett steg inte följer av de föregående underkänns beviset, hur elegant resten än är.

Forskarna beskriver agenten som ett system som söker efter bevis formulerade i Lean. De gav den också tillgång till AlphaProof, ett tidigare DeepMind-system som utvecklats särskilt för matematiska bevis. I forskarnas tester gav en enklare lösning samma resultat: en språkmodell tillsammans med Lean, utan AlphaProof, tog ändå fram alla nio Erdősbevisen (The Decoder). För just de här problemen behövdes alltså inte specialistsystemet.

Artikeln redovisar godkända bevis för de nio Erdős-påståendena och för 44 förmodanden (påståenden som anses sanna men ännu inte har bevisats) ur Online Encyclopedia of Integer Sequences, en omfattande katalog över talmönster (Science). Bland resultaten finns en fråga i två delar om heltal som Erdős och András Sárközy ställde 1970. Den förblev olöst i mer än ett halvt sekel (ABC).

Vad granskaren inte kan avgöra

Leans garanti har en tydlig gräns: den bekräftar att ett bevis styrker exakt det påstående som står i koden. Tre frågor ligger utanför kontrollen: om koden återger vad Erdős avsåg, om någon redan hade besvarat frågan för länge sedan och om svaret lär oss något.

Problemet från 1970 visar varför de två senare frågorna spelar roll. Den andra delen innebär den första, så ett enda bevis räcker för att lösa båda. När agentens bevis började spridas visade det sig att en liten ändring av en konstruktion i originalartikeln från 1970 också besvarar båda delarna (arXiv). Agentens bevis var korrekta. Problemet var helt enkelt närmare en lösning än vad dess status som ”öppet” antydde.

Att upptäcka sådant kräver ämneskunniga forskare. Gergely Bérczi, matematiker vid Aarhus University i Danmark och en av artikelns författare, hjälpte till att välja lämpliga frågor och granska lösningarna (Aarhus University). Han hjälpte också till att skriva versioner av bevisen som människor kan följa. Lean kontrollerade varje rad, medan Bérczi och kollegorna bedömde vad raderna sammantaget tillförde.

Den arbetsfördelningen skiljer studien från det som hände förra månaden. Då formulerade Anthropics Claude om det redan kända beviset för Fermats stora sats i Lean (To Brief). Att översätta ett välkänt bevis väcker inga frågor om originalitet. När AI söker bland påståenden som betraktas som olösta blir frågan om vad som faktiskt är nytt central.

Forskargruppen har publicerat bevisfilerna, så att andra kan låta samma kontrollsystem granska dem (GitHub). Studien visar en avgränsad förmåga: en AI-agent tog fram maskinkontrollerbara bevis för vissa påståenden som matematiker hade betraktat som olösta. Garantin omfattar påståendena så som de formulerats i Lean. Att avgöra vad bevisen tillförde matematiken blev fortsatt en uppgift för matematikerna som läste dem.