AlphaProof Nexus løste 9 av 353 åpne Erdős-problemer, og en enkel løkke klarte de samme

Ni av 353 åpne Erdős-problemer og 44 formodninger fra heltallsdatabasen OEIS: det er fangsten til AlphaProof Nexus, Google DeepMinds system for formelle matematiske bevis, ifølge den fagfellevurderte studien som Science publiserte 8. oktober. Systemet løste også et åpent spørsmål i algebraisk geometri og forbedret en kjent grense innen min-max-optimering, skriver The Decoder.

Kjernen er Gemini 3.1 Pro, som skriver og reviderer bevis i bevisspråket Lean. Lean sjekker hvert utkast etter hver endring, og feilmeldingene styrer neste forsøk. Ved vanskelige delproblemer kan systemet kalle på AlphaProof, DeepMinds spesialiserte bevisverktøy. Bevisene ligger i GitHub-repoet google-deepmind/alphaproof-nexus-results under Apache 2.0, og lake build verifiserer dem på din egen maskin.

Det mest interessante funnet for de som bygger agenter står i studiens egen ablasjon. Ifølge Josep Curto ved Open University of Catalonia (UOC) løste Agent A, en enkel «Ralph loop» som veksler mellom LLM-generering og Lean-verifisering, nøyaktig de samme ni Erdős-problemene som Agent D, den komplette varianten med AlphaProof, evolusjonær algoritme og Elo-rangering mellom subagenter.

«Det er ikke rammeverkets kompleksitet som driver oppdagelsene; det som virkelig flytter nålen, er grunnkapasiteten til LLM-en … kombinert med den direkte, kompromissløse tilbakemeldingen fra den formelle kompilatoren.» — Josep Curto, UOC, til Science Media Centre España

Curto peker også på to svakheter. Kostnadstallene teller bare inferens i vellykkede kjøringer, og for Agent B og D er AlphaProofs egen inferens holdt utenfor. Lean garanterer dessuten bare at beviset holder for påstanden slik den er formalisert, ikke at formaliseringen treffer det matematiske problemet, og studien beskriver flere tilfeller der agentene feilet nettopp der.

Mønsteret er gjenkjennelig fra kodeagenter: en sterk modell i løkke med en streng verifikator, som kompilator eller enhetstester, gir mesteparten av gevinsten, og ekstra orkestrering må forsvare kostnaden sin.