Onuitgebracht Claude-model verhoogt bewezen ondergrens voor zeta-nulpunten naar 67,2 procent

Een onuitgebracht onderzoeksmodel van Claude heeft de bewezen ondergrens voor het aandeel nulpunten van de Riemann-zetafunctie op de kritieke lijn verhoogd van 41,6 naar 67,2 procent, publiceerde Anthropic maandag.

Voor wie werk uitbesteedt aan een model zit het nieuws niet in de wiskunde maar in het bewijsstuk eronder. Het resultaat staat volledig in Lean, een bewijsassistent die elke redeneerstap machinaal narekent. De publieke code bevat geen enkele openstaande stap en steunt op geen andere aannames dan de drie standaardaxioma's van wiskundebibliotheek Mathlib. Dit is dus geen output die plausibel klinkt, maar output waar een controle overheen ging die onafhankelijk van het model kan falen.

De kanttekening staat er meteen bij. De Riemann-hypothese zelf is niet bewezen, Anthropic verwacht ook niet dat deze techniek daarheen leidt, en het model is een onderzoeksversie zonder releasedatum. Er valt vandaag niets aan te schaffen of in te richten.

Van 5/12 naar twee derde

Het paper heet "More than two thirds of the zeros of the Riemann zeta function lie on the critical line" en vermeldt één auteur: Claude. De hoofdstelling zegt onvoorwaardelijk dat van de nulpunten in een venster tussen T en 2T asymptotisch minstens twee derde op de kritieke lijn ligt. Met een geoptimaliseerde testfamilie wordt die constante 0,6725, en twee vervolgstellingen leveren eenzelfde aandeel nulpunten die zowel enkelvoudig zijn als op de lijn liggen, plus een aandeel van 0,83625 verschillende nulpunten.

Het vorige record stond sinds 2020 op 5/12, ongeveer 41,7 procent, van Pratt, Robles, Zaharescu en Zeindler. De lijn daarnaartoe loopt via Selberg, Levinson en Conrey en deed er tachtig jaar over. Het nieuwe ingrediënt is geen nieuwe analyse: het paper leest een bestaande som uit werk van Baluyot, Goldston, Suriajaya en Turnage-Butterbaugh met lineaire algebra, gecombineerd met een observatie van Enrico Bombieri uit 2000.

Zesendertig uur, zestig subagents, 31 miljoen tokens

Een medewerker van Anthropic zonder gevorderde wiskundige opleiding vroeg het model een serieuze poging te doen. Het model werkte daarna ongeveer zesendertig uur zelfstandig door, testte zo'n 650 benaderingen, verdeelde het werk over ongeveer zestig subagents in twee sessies en verbruikte 31 miljoen uitvoertokens. Onderweg draaide het zo'n 2.400 shell-opdrachten en haalde het 54 arXiv-papers op om te controleren of het resultaat echt nieuw was.

De transcriptie in appendix C van het paper laat zien dat het model de opdracht eerst weigerde. Aangespoord om in zichzelf te geloven, antwoordde het dat alle 106 overgebleven ideeën uit een eerdere sessie in vier categorieën vielen, van een herformulering van een bekende stelling tot iets dat de reviewers zelf bijna-tautologisch noemden, en dat vertrouwen geen invoer is voor een bewijs. Toen er wél iets stond, was de eerste reactie ongeloof: het record lag op 41,7 procent en daar was tachtig jaar over gedaan.

De controle die het verschil maakte

Het model zette drie blinde vijandige reviewers op het argument, elk met een eigen toegewezen faalmodus, plus een vierde voor de technische benaderingen en een agent die de priemzijde blind opnieuw afleidde. Alle drie hielden stand. Op zichzelf zegt dat weinig, want een controle telt pas als hij onafhankelijk kan falen van wat hij controleert en een tweede taalmodel deelt de blinde vlek van het eerste.

Wat het resultaat wél draagt zijn controles van een andere soort. De formalisering in Lean, georkestreerd door Anthropic-medewerker Eric Easley, is regel voor regel na te rekenen op GitHub: het commando dat de gebruikte aannames opsomt geeft alleen de drie standaardaxioma's terug, zonder onbewezen tussenstap. Von Neumanns spoorongelijkheid en beide richtingen van de traagheidswet van Sylvester zaten nog niet in Mathlib en zijn door dit werk toegevoegd. Een symbolische hercontrole bevestigde 31 hoofdconstanten; de asymptotische foutgrenzen vallen daarbuiten en zijn analytisch bewezen. Twee externe getaltheoretici, Brian Conrey en Daniel A. Goldston, lazen het manuscript.

Elf dagen na de tien bewijzen van OpenAI

Het patroon is niet nieuw. OpenAI bevestigde op 1 augustus zijn volgende model Astra door tien bewijzen te publiceren voor wiskundeproblemen die minstens tien jaar openstonden, met een tokenrekening van ongeveer tweeduizend dollar eronder. Anthropic noemt geen bedrag, wel een verbruik van 31 miljoen uitvoertokens. Beide keren komt de aankondiging van een model dat niemand kan afnemen, en is het wiskundige resultaat het bewijsstuk voor de capaciteit.

Wat hier verschuift is niet dat AI beter wordt in wiskunde. Het is dat het werk aankomt in een vorm die iets anders dan een taalmodel kan narekenen. Waar zo'n vorm bestaat, een formeel bewijs, een testsuite die rood wordt, een saldo dat aansluit of niet, kan een model veel langer zelfstandig doorwerken voordat iemand meeleest. Waar die vorm ontbreekt, blijft er een tekst over die overtuigend klinkt en die je regel voor regel moet nalopen. Die grens bepaalt welk werk je vandaag aan een agent durft te geven, veel meer dan de score op een benchmark.