EnglishTien AI-agents leveren in vijftien uur een computerbewijs voor een puzzel met zeven elektronen
Het bedrijf Vals AI liet tien AI-agents in vijftien uur een bewijs schrijven voor een ruim honderd jaar oude puzzel: hoe zeven elektronen op een bol gaan liggen. Een computer controleerde elke stap. De volgende stap is een beoordeling door wiskundigen.
Zet een paar elektronen op een bol. Ze stoten elkaar af en schuiven net zo lang op tot de totale energie zo laag mogelijk is. Welke vorm krijgen ze dan? De Britse natuurkundige J.J. Thomson stelde die vraag in 1904, toen hij probeerde te begrijpen hoe elektronen in een atoom zitten. Sindsdien heet het het Thomson-probleem.
Voor zeven elektronen kennen onderzoekers het antwoord al tientallen jaren uit computerberekeningen: vijf elektronen in een ring rond de evenaar en één op elke pool. Samen vormen ze een dubbele piramide met een vijfhoek als grondvlak. Maar een berekening die steeds dezelfde vorm vindt, is nog geen bewijs. Er zijn oneindig veel manieren om zeven punten op een bol te zetten, en een bewijs moet laten zien dat geen enkele daarvan minder energie heeft. Zo'n bewijs bestond alleen voor een paar aantallen: 2, 3, 4, 6 en 12 elektronen, voor 5 elektronen sinds 2013 met hulp van de computer, en voor 8 elektronen sinds september van dit jaar.
Tien agents, één bewijs
Eind september meldde Hung Tran van Vals AI, een bedrijf dat AI-modellen test en vergelijkt, dat het nu ook voor zeven elektronen is gelukt. Tran zette tien AI-agents aan het werk: AI-programma's die zelfstandig taken uitvoeren, in dit geval allemaal met het model Claude Sonnet 5.5 van Anthropic. Ze kregen de precieze opdracht, een gedeeld prikbord om te overleggen en negen mogelijke aanpakken. Een daarvan was de methode overnemen die kort daarvoor bij acht elektronen had gewerkt. De agents mochten zelf kiezen welke aanpakken ze doorzetten, samenvoegden of lieten vallen.
Na ongeveer vijftien uur en 1.270 berichten lag er een bewijs. Eén agent nam zelf de rol van samensteller op zich en voegde alle goedgekeurde stukken samen in één bestand van 17.895 regels. Het bewijs zegt twee dingen: geen enkele stand van zeven elektronen heeft minder energie dan de dubbele piramide, en elke stand met precies die energie is dezelfde dubbele piramide, alleen gedraaid of gespiegeld.
Een computer controleert elke stap
Het bewijs is geschreven in Lean, een programmeertaal voor wiskunde. Elke stap staat er zo precies in dat software kan nagaan of hij klopt. Daardoor hoef je de AI niet op haar woord te geloven. Volgens Tran keurde Lean het bewijs goed, en vond ook een tweede, apart gebouwd controleprogramma geen fouten. Als proef veranderde hij één getal in het bewijs, waarna dat tweede programma het meteen afkeurde. Het bewijs staat openbaar op GitHub, zodat iedereen de controle zelf kan herhalen.
Hoe het bewijs werkt
Alle oneindig veel standen uitproberen kan niet. Daarom werkt het bewijs met een ondergrens: een getal waarvan vaststaat dat de energie nooit lager kan uitkomen. Valt die ondergrens precies samen met de energie van de dubbele piramide, dan kan geen andere stand beter zijn.
Voor zeven elektronen lukt dat niet in één keer. Het bewijs deelt alle mogelijke standen daarom op in groepen. Het kijkt daarbij naar het paar elektronen dat het dichtst bij recht tegenover elkaar ligt, want in de dubbele piramide liggen de twee polen precies tegenover elkaar. Liggen er nergens twee elektronen bijna tegenover elkaar, dan blijft de energie altijd duidelijk boven die van de piramide. De standen waarin dat wel zo is, worden in kleinere stukken nagelopen. Wat overblijft, zijn standen die bijna gelijk zijn aan de piramide zelf. Een laatste, heel precieze rekenstap laat zien dat de piramide daar het laagste punt is.
De getallen voor al die grenzen zocht een rekenprogramma eerst op. Zo'n programma rekent met afgeronde kommagetallen en maakt daardoor kleine fouten. Daarom zijn de getallen daarna omgezet in exacte breuken, die Lean zelf narekent. Het bewijs hangt dus niet af van het programma dat de getallen vond.
Wat er nog moet gebeuren
Tran zegt er zelf bij dat wiskundigen het bewijs nog niet hebben beoordeeld en dat het niet in een vakblad is verschenen. Lean laat zien dat het bewijs klopt bij de opdracht zoals die in Lean is opgeschreven. Vakgenoten kunnen nu nagaan of die opdracht precies het Thomson-probleem beschrijft. De controles deed Vals AI zelf; omdat alles openbaar staat, kunnen anderen ze herhalen.
Jason Rute, die werkt aan wiskunde die computers kunnen controleren, noemde het resultaat indrukwekkend. Het eerdere bewijs voor vijf elektronen was volgens hem een losse computerberekening waarvan niet eens duidelijk was of die in Lean te zetten was. Het gaat wel om zeven elektronen; voor elk aantal geldt een eigen puzzel.
Op naar tien, negen en tweeëndertig
Op 27 oktober legde Vals-onderzoeker Jacob Stavrianos uit hoe het bewijs werkt en welke aantallen hierna kunnen. Volgens de berekeningen van het bedrijf zou dezelfde aanpak eerst voor tien en daarna voor negen elektronen moeten werken. Bij 32 elektronen, die naar verwachting verdeeld liggen zoals de vlakken van een klassieke voetbal, schiet de methode volgens Vals AI tekort en is een nieuw idee nodig. De opdrachten voor 9, 10 en 32 elektronen staan op de site Prove2Me, waar iedereen een bewijs kan insturen.
Teams van AI-agents die met Lean werken, laten nu op meer plekken van zich horen. Bij Axiom Math zetten tientallen agents een bestaand bewijs van zo'n 15.000 pagina's om in code die een computer controleert. Daar ging het om een bewijs dat mensen al hadden geschreven. Bij Vals AI bedachten de agents zelf een bewijs voor een geval waarvoor nog geen bewijs bestond.
Wat betekent dit voor de weg naar de singulariteit?
Tien AI-agents verdeelden zelf het werk, overlegden, lieten doodlopende aanpakken vallen en voegden de stukken samen tot één bewijs voor een open wiskundevraag. Dat is meer dan een antwoord geven: het is zelfstandig onderzoek doen, in een paar uur in plaats van jaren. En omdat een computer elke stap controleert, hoeft niemand de AI blind te vertrouwen. Die combinatie maakt het mogelijk om AI steeds grotere onderzoeksvragen te geven. De volgende proef is of dezelfde aanpak ook tien en negen elektronen aankan, en wie het nieuwe idee vindt voor 32.
