Een studie van Google DeepMind, gepubliceerd op 8 oktober 2026, rapporteerde dat AlphaProof Nexus 9 van 353 geformaliseerde Erdős-problemen oploste en 44 van 492 geselecteerde vermoedens uit de Online Encyclopedia of Integer Sequences (OEIS) bewees. Het systeem combineert taalmodellen met Lean, een bewijsassistent die formele wiskundige bewijzen mechanisch controleert.
Wat AlphaProof Nexus doet
AlphaProof Nexus is een raamwerk voor het zoeken naar formele bewijzen. Het neemt als invoer een stelling die in Lean is vastgelegd, met een bewijsschets: een eerste, nog onvolledige versie van een bewijs. Extra context in gewone taal kan worden meegegeven; wiskundige voorkennis kan ook in Lean worden gecodeerd.
Een taalmodel past de bewijsschets aan en Lean controleert de formele uitkomst. Als het bewijs niet compileert, levert Lean feedback waarmee de agent een volgende poging kan doen. Zo wordt een voorstel niet alleen op aannemelijkheid beoordeeld: het moet ook voldoen aan de formele regels van de stelling.
Wat de resultaten meten
De studie rapporteerde resultaten voor twee verschillende verzamelingen. De Erdős-problemen kwamen uit de formele stellingen die op dat moment beschikbaar waren in de repository Formal Conjectures. De 353 items vormden dus de geëvalueerde, geformaliseerde deelverzameling. De OEIS-test betrof afzonderlijk geselecteerde open vermoedens.
| Geëvalueerde verzameling | Bewezen | Omvang van de evaluatie | Afbakening |
| Geformaliseerde Erdős-problemen | 9 | 353 problemen | De formele stellingen in Formal Conjectures die voor de evaluatie beschikbaar waren |
| Geselecteerde OEIS-vermoedens | 44 | 492 vermoedens | Een selectie van open vermoedens uit de OEIS |
Twee van de negen opgeloste Erdős-vragen stonden al 56 jaar open. Dat is een opvallend resultaat binnen die testset, maar de meeste geëvalueerde Erdős-problemen bleven onopgelost.
Hoe het bewijszoeken werkt
De basisagent laat meerdere taalmodelagents bewijsschetsen aanpassen. Lean controleert de pogingen en geeft feedback. De uitgebreidere configuratie voegt een zoekproces toe waarin schetsen worden gerangschikt en kansrijke varianten verder worden ontwikkeld. Die configuratie kan ook AlphaProof inzetten om deelproblemen aan te pakken.
De grens van die aanpak ligt bij de formele invoer: de beschreven werkwijze begint met een Lean-stelling en bewijsschets. De studie beschrijft geen proces dat een willekeurige wiskundige vraag in gewone taal zelfstandig omzet in zo’n formele stelling.
Wat de resultaten wel en niet laten zien
Lean controleert of een bewijs de ingevoerde formele stelling volgt. Die controle bepaalt op zichzelf niet of de formalisering precies overeenkomt met de oorspronkelijke informele wiskundige vraag. Voor de Erdős-stellingen beschrijven de onderzoekers daarom ook deskundige beoordeling van de formaliseringen.
De studieauteurs melden dat de successen vooral lagen in combinatoriek, convexe optimalisatie en getaltheorie, gebieden waarin de wiskundige bibliotheken van Lean verder zijn ontwikkeld. AlphaProof Nexus behaalde daarmee resultaten op specifieke formele testsets; de reikwijdte van die uitkomsten hangt samen met de gekozen problemen en hun formalisering.
