Vad artikeln hävdar
Ett team på Google DeepMind har publicerat en kollegialt granskad redogörelse för ett AI-system som hittar matematiska bevis och får dem maskinkontrollerade efter hand. Artikeln, “Advancing Mathematics Research with AI-Driven Formal Proof Search” av Tsoukalas med kollegor, publicerades i Science den 8 oktober.
Systemet, AlphaProof Nexus, är byggt kring Gemini 3.1 Pro. Det skriver ett bevis i Lean, ett formellt språk där varje logiskt steg kontrolleras av programvara, och kontrollantens felmeddelanden styr nästa utkast. För svårare delproblem kan det lämna över till AlphaProof, DeepMinds specialiserade bevisverktyg.
Forskarna valde ut 353 öppna problem ur Erdős samling och kodade dem i Lean. Systemet löste nio av dem — omkring 2,5% — varav två hade stått olösta i 56 år. Det bevisade också 44 förmodanden ur On-Line Encyclopedia of Integer Sequences, avgjorde en öppen fråga i algebraisk geometri och förbättrade en känd gräns i min-max-optimering, en teknik som används när vissa AI-modeller tränas.
Ablationen är det intressanta
DeepMind uppger att systemet löste samma nio Erdősproblem utan AlphaProof. En ablationsanalys fann att en enklare uppsättning, som artikeln kallar Agent A, nådde samma nio — en punkt som Josep Curto vid Universitat Oberta de Catalunya tar upp i expertkommentarer som samlats in av Science Media Centre España. Curto läser resultatet som ett tecken på överkonstruktion och menar att artikeln bär på metodologiska inkonsekvenser.
Hans skarpare invändning gäller vad formell verifiering köper och inte köper. Lean, påpekar han, garanterar att ett bevis är logiskt giltigt. Det garanterar inte att påståendet någon formaliserat är det problem de menade att formulera. Översättningen från en informell förmodan till Lean är fortfarande ett mänskligt steg, och ett fel där överlever kontrollanten orört.
Hur nio av 353 ska läsas
Nämnaren spelar roll. Det här är nio framgångar ur en avgränsad mängd som teamet valde och formaliserade, inte en allmän förmåga att plocka ned berömda förmodanden. Pablo Haya Coll vid Madrids autonoma universitet pekar i samma kommentarsamling på metoden snarare än antalet: värdet ligger i ett upprepbart sätt att framställa matematiska upptäckter, inte i de nio.
Javier Aramayona, som leder Spaniens institut för matematiska vetenskaper, tar upp det problem som följer av att maskinkontrollerade bevis anländer snabbare än någon hinner läsa dem: många AI-genererade resultat är verifierade och ändå inte helt förstådda. Teodoro Calonge vid universitetet i Valladolid kallade det en artikel av hög kvalitet och ett tidigt försök, med stort utrymme för förbättring.
Kontrasten mot det andra laboratoriet
Vägen det här arbetet tog är i sig en del av historien. DeepMind lade ut Erdőslösningarna offentligt innan artikeln kom, och lät sedan arbetet gå genom kollegial granskning. OpenAI tog den andra vägen och publicerade hundratals AI-genererade bevis i ett kodarkiv, vilket fick en grupp matematiker att kräva bojkott av företaget tidigare i månaden.
Det som är värt att följa är om Lean-filerna håller för extern granskning, och om någon av de nio formaliseringarna visar sig uttrycka något annat än det Erdősproblem den är märkt med. Den kontrollen är nu tillgänglig för vem som helst, vilket är det praktiska argumentet för den väg DeepMind valde.
