EnglishGoogle laat AI-agentteams een wiskundig vermoeden uit 2013 helpen bewijzen
Met /teamwork in Antigravity werkten AI-agents van Google samen met onderzoekers aan een bewijs voor het Courtade-Kumar-vermoeden uit 2013. Een computer controleerde elke stap van het bewijs.
Google heeft nieuwe resultaten gemeld van /teamwork, een functie in Antigravity, het programmeerplatform van Google waarin AI-agents zelf werk uitvoeren. liet Google in Antigravity al een team van AI-agents samen programmeren met /swarm. Bij /teamwork werken zulke teams niet alleen aan code, maar ook aan wiskundig onderzoek.
Bij /teamwork krijgen de agents verschillende rollen. De ene werkt een oplossing uit, de andere zoekt naar fouten, en een agent die vastloopt draagt zijn taak over aan een nieuwe. Menselijke experts bepalen de vragen en beoordelen de uitkomsten. Voor de nieuwe resultaten gebruikte Google vooral Gemini 4 Argon, het zwaarste AI-model dat Google eind oktober 2026 uitbracht. Het werk is volgens Google de afgelopen weken gedaan.
Een oud vermoeden bewezen
Een vermoeden is in de wiskunde een bewering die veel onderzoekers voor waar houden, maar die nog niemand heeft bewezen. Het Courtade-Kumar-vermoeden uit 2013 gaat over een reeks enen en nullen waarvan een kopie door ruis is aangetast: hier en daar is een 1 een 0 geworden, of andersom. Hoeveel kan één enkele uitkomst, berekend uit de oorspronkelijke reeks, verraden over die beschadigde kopie? Het vermoeden zegt dat je het meeste te weten komt als die uitkomst gewoon één van de oorspronkelijke enen of nullen is. Die vraag doet ertoe voor de theorie van hoe informatie door een storende verbinding komt.
Onderzoekers van Google, de Chinese Universiteit van Hongkong, de University of Southern California en Carnegie Mellon University bewezen het vermoeden samen met de AI-agents. Het bewijs verscheen in september 2026 als voorpublicatie. De onderzoekers uit Hongkong bedachten de aanpak die het probleem terugbracht tot een rekenprobleem met veertien onbekenden. Volgens Google werkten Argon en eerdere Gemini-modellen daarna het grootste deel van de benodigde rekenstappen en controles uit.
Het hele bewijs is omgezet in 50 miljoen regels Lean, een programmeertaal waarmee een computer elke logische stap van een bewijs nakijkt. Rond dezelfde tijd zetten ook andere wiskundigen bewijzen van dit vermoeden online.
Ook bekende bewijzen nagekeken
Google meldt ook dat /teamwork met Argon de Weil-vermoedens helemaal zelfstandig in Lean heeft omgezet, in ongeveer 1,8 miljoen regels. Die vermoedens over het tellen van oplossingen van vergelijkingen bewees de Belgische wiskundige Pierre Deligne al in 1974. Nieuw is dus niet het bewijs zelf, maar dat een AI-systeem zo'n groot en beroemd bewijs zonder hulp in een vorm zette die een computer kan controleren.
Eerder, in augustus 2026, liet Google al zien dat agentteams met het oudere Gemini 3.1 Pro zeven open problemen uit de theoretische informatica oplosten. Menselijke experts keurden er zes goed; het zevende bewijs, van ruim veertig bladzijden, werd door de computer in Lean gecontroleerd.
Ontwikkelaars met een betaald abonnement kunnen /teamwork zelf gebruiken in Antigravity. Google biedt daarnaast 10.000 onderzoekers aan universiteiten zes maanden gratis toegang tot de zwaarste versie.
Wat betekent dit voor de weg naar de singulariteit?
Computers die elke stap van een bewijs nakijken, bestaan al lang. Het probleem was dat iemand al die stappen eerst moest uitschrijven, en dat kostte wiskundigen soms jaren. Als AI-agents dat schrijfwerk zelf doen, in miljoenen regels per keer, wordt zo'n controle goedkoop. Een wiskundige kan dan bij een nieuw bewijs meteen een computercontrole meeleveren, zodat vakgenoten niet maandenlang hoeven na te rekenen of het klopt.
Als die lijn doorzet, helpt dat AI ook zelf verder. Een bewijs dat de computer heeft goedgekeurd, is een antwoord waarvan zeker is dat het goed is. Een AI-model dat van zulke antwoorden leert, kan steeds moeilijkere problemen aan zonder dat een mens elk antwoord hoeft na te lopen. Andere AI-bedrijven moeten dan ook laten zien dat hun modellen werk leveren dat een computer kan controleren, en niet alleen tekst die overtuigend klinkt. Mensen blijven nodig om te kiezen welke vragen de moeite waard zijn, en om na te gaan of de stelling die de computer controleert echt het probleem beschrijft dat ze bedoelden.
