Hvad artiklen hævder
Et hold i Google DeepMind har offentliggjort en fagfællebedømt redegørelse for et AI-system, der finder matematiske beviser og får dem maskinkontrolleret undervejs. Artiklen, “Advancing Mathematics Research with AI-Driven Formal Proof Search” af Tsoukalas med kolleger, udkom i Science den 8. oktober.
Systemet, AlphaProof Nexus, er bygget omkring Gemini 3.1 Pro. Det skriver et bevis i Lean, et formelt sprog hvor hvert logisk skridt kontrolleres af software, og kontrollantens fejlbeskeder styrer næste udkast. Til sværere delproblemer kan det overlade arbejdet til AlphaProof, DeepMinds specialiserede bevisværktøj.
Forskerne udvalgte 353 åbne problemer fra Erdős-samlingen og kodede dem i Lean. Systemet lukkede ni af dem — omkring 2,5% — og to af dem havde stået uløste i 56 år. Det beviste også 44 formodninger fra On-Line Encyclopedia of Integer Sequences, afgjorde et åbent spørgsmål i algebraisk geometri og forbedrede en kendt grænse i min-maks-optimering, en teknik der bruges når visse AI-modeller trænes.
Ablationen er det interessante
DeepMind oplyser, at systemet løste de samme ni Erdősproblemer uden AlphaProof. En ablationsanalyse fandt, at en enklere opsætning, som artiklen kalder Agent A, nåede de samme ni, et punkt Josep Curto fra Universitat Oberta de Catalunya rejser i ekspertkommentarer indsamlet af Science Media Centre España. Curto læser resultatet som et tegn på overkonstruktion og mener, at artiklen bærer metodiske uoverensstemmelser.
Hans skarpeste indvending handler om, hvad formel verifikation køber og ikke køber. Lean, bemærker han, garanterer at et bevis er logisk gyldigt. Det garanterer ikke, at den påstand nogen formaliserede, er det problem de mente at formulere. Oversættelsen fra en uformel formodning til Lean er stadig et menneskeligt skridt, og en fejl dér overlever kontrollanten urørt.
Hvordan ni ud af 353 skal læses
Nævneren betyder noget. Det er ni succeser i en afgrænset mængde, holdet selv valgte og formaliserede, ikke en generel evne til at fælde berømte formodninger. Pablo Haya Coll fra Universidad Autónoma de Madrid peger i den samme kommentarsamling på metoden frem for tallet: værdien ligger i en gentagelig måde at frembringe matematiske opdagelser på, ikke i de ni.
Javier Aramayona, der leder Spaniens institut for matematiske videnskaber, rejser det problem, der følger af at maskinkontrollerede beviser ankommer hurtigere, end nogen når at læse dem: mange AI-genererede resultater er verificerede og alligevel ikke fuldt forstået. Teodoro Calonge fra Universitetet i Valladolid kaldte det en artikel af høj kvalitet og et tidligt forsøg med betydeligt rum for forbedring.
Kontrasten til det andet laboratorium
Den vej, dette arbejde tog, er i sig selv en del af historien. DeepMind lagde Erdősløsningerne offentligt frem, før artiklen udkom, og sendte derefter arbejdet gennem fagfællebedømmelse. OpenAI valgte den anden vej og lagde hundredvis af AI-genererede beviser i et kodelager, hvilket fik en gruppe matematikere til at kræve boykot af virksomheden tidligere på måneden.
Det, der er værd at følge, er om Lean-filerne holder til ekstern granskning, og om nogen af de ni formaliseringer viser sig at udtrykke noget andet end det Erdősproblem, de er mærket med. Den kontrol er nu til rådighed for enhver, hvilket er det praktiske argument for den vej, DeepMind valgte.
