Claude sloot Fermat in 11 dagen af: 13,4 miljoen regels Lean en geen enkele “duidelijk”

Op 4 september toonde Anthropic de allereerste volledige machinetest van de laatste stelling van Fermat. Claude vertaalde in 11 dagen, bijna zonder de hulp van mensen, het bewijs van Andrew Wiles in de taal Lean: 13,4 miljoen regels code, ongeveer 30.000 tussenliggende stellingen, nul “duidelijk uit wat er is gezegd.” Het project, waar wiskundigen al jaren plannen voor hadden - alleen de tekening van de eerste fase van Kevin Buzzard van het Imperial College London was 86 pagina's lang - werd in anderhalve week voltooid.

Laten we meteen duidelijk maken wat hier niet staat: er is geen nieuw bewijs. Het model heeft geen eigen pad naar de stelling bedacht. Ze deed iets anders, en eerlijk gezegd niet minder complex: ze nam een ​​menselijk bewijs, waarbij op elke pagina disclaimers staan ​​als 'dit volgt triviaal', en herschreef het zodat de compiler elke stap controleert. Wiskundigen hadden na 1995 99,9% vertrouwen in de stelling. Nu kun je honderd procent gaan: Lean heeft de hele afleiding van de drie standaardaxioma's doorlopen, en er valt niets meer te twijfelen.

Wat heeft de computer precies gecontroleerd?

Cijfers zijn hier geschikter dan scheldwoorden.

• De 13,4 miljoen regels van Lean zijn meer dan vijf keer groter dan de gehele Mathlib, de belangrijkste formele wiskundebibliotheek van het systeem.
• Er zijn ongeveer 30.000 tussenliggende stellingen bewezen; de uiteindelijke productie betrof ongeveer 29.500.
• Het compileren van een repository op een machine met 96 kernen duurt ongeveer 20 keer langer dan het compileren van Mathlib. Buzzard kreeg tijdens de test een server met 500 GB RAM.
• Er wordt alleen vertrouwd op drie standaardaxioma's Lean. Geen ‘aannames voor eenvoud’.

Kevin Buzzard, dezelfde wiskundige die sinds 2024 het Fermat-formalisatieproject voor de gemeenschap leidt, heeft de repository gedownload, samengesteld en de comparator uitgevoerd: de outputformulering van de stelling valt samen met de referentie uit Mathlib, alle vinkjes zijn groen. Zijn recensie: “een buitengewone prestatie van automatische formalisering.”

Eén regel in de marge, drie en een halve eeuw werk

Rond 1637 schreef Pierre de Fermat de bewering toe aan de kantlijn van Diophantus 'Rekenkunde: voor n groter dan twee heeft de vergelijking aⁿ + bⁿ = cⁿ geen oplossingen in natuurlijke getallen. Hieronder staat een zin die een legende is geworden: “Ik heb een werkelijk prachtig bewijs gevonden, maar de marges zijn er te smal voor.” Generaties wiskundigen, van Euler tot Kummer, gingen in stukjes naar het resultaat toe. In 1908 werd een prijs van 100.000 goudmarken toegekend voor het bewijs, en in het eerste jaar werden 621 onjuiste oplossingen ontvangen.

In juni 1993 presenteerde Andrew Wiles zijn bewijs tijdens een lezingenreeks in Cambridge. Twee maanden later stelde een recensent een vraag waaruit bleek dat er een gat in een van de ontwerpen zat. Een jaar lang repareerde Wiles het - eerst alleen, daarna samen met oud-student Richard Taylor - en stond op het punt het allemaal op te geven, en in 1995 publiceerde hij een tekst van 129 pagina's. De laatste, “technische” vraag bleef bestaan: is het mogelijk om de computer te dwingen dit alles in zijn geheel te bevestigen?

Geen nieuw bewijs, maar een nieuwe kans

Het is gebaseerd op de analyse van Darmon, Diamond en Taylor uit 1995 van het Wiles-Taylor-argument via de stelling van Langlands-Tunnell en de afdaling van het Ribet-niveau. Het idee om Wiles te formaliseren werd in de jaren 2000 geuit door de Nederlandse computerwetenschapper Jan Bergstra, maar tot voor kort werd dit beschouwd als werk voor een hele wetenschappelijke richting. Individuele gevallen - vierdegraads, gewone eenvoudige gevallen - werden eerder verplaatst naar Lean. Met de nieuwe repository is Weidiks volledige lijst van 100 formalisatietaken gesloten: de benchmark waarmee dit gebied werd vergeleken is twintig jaar oud.

Buzzard schrijft trouwens eerlijk: wiskundig gezien onthult het werk niets nieuws - hij geloofde al in Wiles. De waarde ligt ergens anders. Het beoordelen van een nieuw wiskundeartikel duurt maanden of zelfs jaren; Als aan een machine kan worden gevraagd om een ​​bewijs on-the-fly te formaliseren, zal de peer review afnemen en zullen verborgen aannames op expertniveau aan de oppervlakte komen. Voor de wetenschap, waar alles afhangt van de eerlijkheid van conclusies, is dit een serieuze verschuiving.

Hoe die 11 dagen er van binnen uitzagen

Het werk werd geleid door Tianyi Peng, een antropisch onderzoeker die eerder een groep AI-formalisatietools had samengesteld aan de Columbia University. Volgens hem was hij aanvankelijk niet van plan het einde te bereiken: hij wilde alleen maar zien hoeveel Claude het project van Buizerd zou bevorderen. Gepromoveerd naar de finale.

Veel agenten werkten parallel: sommige voltooiden wiskundige definities, andere bestormden tussenliggende lemma's, weer anderen gingen hogerop in de stellingenboom, en weer anderen brachten de onderdelen weer samen tot één enkele conclusie. De eerste dagen gingen mis: de agenten verloren het algemene beeld van het project en ongeveer zeven procent van de eerste pogingen bleef in de uiteindelijke code staan. De ommekeer vond plaats toen het team werd overgezet naar het Prove2Me-platform: het bewijs daarin is een grafiek van stellingknooppunten, waar je kunt zien wat al bewezen is, wat er nog op de vereisten wacht en wat je vervolgens moet doen. Verklaringen worden gescheiden van bewijzen, de compilatie wordt versneld en elke stelling heeft een doorzoekbare tekstbeschrijving. De omvang van het werk bedraagt ​​ongeveer zes miljard outputtokens, en menselijke aanwijzingen werden teruggebracht tot een hoog niveau: “deze richting is een prioriteit.”

Waar te kijken

De repository is op GitHub geplaatst - als je wilt, kun je de controle zelf uitvoeren als je een machine hebt met 96 cores en sterke zenuwen. Primaire bronnen: analyse van Anthropic En Het bericht van Buizerd op de Xena Project-blog.

En als je na een verhaal met 13 miljoen regels wilt zien hoe moderne modellen omgaan met kleinere taken - algoritmen, code, berekeningen - kijk dan eens naar de secties "Code" En "Chatten" op NeuralSpace: daar kun je experimenteren met modellen en deze via de API aan je projecten koppelen.