AI agent van Google lost 9 'onmogelijke' wiskunde problemen op

Google DeepMind heeft op een AI-agent gepresenteerd die zelfstandig 9 open Erdős-problemen heeft opgelost. De agent, AlphaProof Nexus, gebruikt grote taalmodellen en de formele bewijstaal Lean om wiskundige redeneringen automatisch te controleren. Volgens de paper loste het systeem ook 44 van 492 open OEIS-vermoedens op en droeg het bij aan onderzoek in optimalisatie, grafentheorie, algebraïsche meetkunde en kwantumoptics.

AlphaProof Nexus maakt AI bruikbaarder voor echt wiskundig onderzoek, omdat elk bewijs formeel wordt gecontroleerd. Grote taalmodellen kunnen overtuigende maar foutieve redeneringen geven. Lean voorkomt dat risico door elke logische stap te verifiëren voordat een bewijs wordt geaccepteerd.

De onderzoekers noemen vooral de combinatie van taalmodel, compiler-feedback en formele bewijszoektocht belangrijk. De agent werkt niet alleen als tekstgenerator, maar als een systeem dat hypothesen probeert, fouten terugkrijgt en zijn aanpak aanpast.

Google DeepMind testte AlphaProof Nexus op 353 formeel vastgelegde Erdős-problemen. De meest uitgebreide agent loste daarvan 9 op, tegen rekencosten van enkele honderden dollars per probleem. Een eenvoudiger agent zonder alle extra functies wist achteraf dezelfde 9 problemen ook te bewijzen, maar was bij de lastigste gevallen duurder.

Daarnaast bewees het systeem 44 open vermoedens uit de Online Encyclopedia of Integer Sequences. De onderzoekers melden ook dat de agent een 15 jaar oude open vraag over Hilbert-functies oploste en een betere convergentiegarantie vond voor een optimalisatie-algoritme.

AlphaProof Nexus krijgt een wiskundig probleem binnen als Lean-bestand met een ontbrekend bewijs. De agent mag binnen afgebakende delen nieuwe lemma’s, definities en bewijsstappen toevoegen. Daarna controleert Lean automatisch of het bewijs klopt.

De volledige agent gebruikt meerdere rollen. Een prover-subagent zoekt naar bewijzen, een validator controleert de uitkomst en een rater-subagent beoordeelt welke tussenpogingen veelbelovend zijn. Die pogingen worden opgeslagen in een populatiedatabase met Elo-scores, vergelijkbaar met een ranglijst.

De resultaten tonen dat AI steeds meer verschuift van hulp bij tekst naar hulp bij formele ontdekking. Dat is een belangrijke stap voor onderzoek, omdat wiskundigen minder tijd hoeven te besteden aan het controleren van volledige redeneringen en meer aandacht kunnen geven aan moeilijke tussenstappen.

De onderzoekers blijven voorzichtig. De meeste Erdős-problemen bleven onopgelost, en het systeem werkt vooral goed in domeinen waar Lean al sterke wiskundige bibliotheken heeft. Toch laat de paper zien dat AI-agenten niet alleen bestaande bewijzen kunnen opschrijven, maar ook nieuwe formeel controleerbare routes kunnen vinden.