AI van Anthropic formaliseert bewijs van Fermats laatste stelling in 11 dagen

Van bewijs naar controleerbare code

Fermats laatste stelling is een van de beroemdste resultaten uit de wiskunde. Het Franse genie Pierre de Fermat beweerde in 1637 dat er geen gehele getallen x, y en z bestaan die voldoen aan x^n + y^n = z^n, als n groter is dan 2. Hij liet geen bewijs na. Pas in 1994 leverden de wiskundigen Andrew Wiles en Richard Taylor het sluitende bewijs, na jaren van werk in geavanceerde wiskunde. De stelling behoort tot de getaltheorie, het vakgebied dat draait om de eigenschappen van gehele getallen. Nu heeft AI-bedrijf Anthropic dat bewijs omgezet in code die een computer regel voor regel controleert op fouten. Dat proces heet autoformalisatie: het vertalen van menselijke wiskundige redeneringen naar een taal die machines kunnen verifiëren. Anthropic gebruikte daarvoor een geavanceerd, nog niet uitgebracht prototype van chatbot Claude. Het resultaat is een bewijs van 13 miljoen regels code, geschreven in de programmeertaal Lean. Bij Lean-formalisering checkt een computer stap voor stap of elke logische stap in een bewijs klopt, zodat er geen ruimte overblijft voor menselijke vergissingen.

Tien jaar werk in elf dagen

Wat vooral opvalt, is de snelheid. Wiskundigen schatten vooraf dat het formaliseren van het Fermat-bewijs zeker tien jaar zou kosten als mensen het met de hand zouden doen. Claude deed het in elf dagen. Anthropic maakte de doorbraak op 4 september bekend. Wiskundige Alex Kontorovich van Rutgers University noemt het resultaat verbijsterend. Ook Kevin Buzzard van Imperial College London, die eerder meewerkte aan formalisatieprojecten, zegt dat de complexiteit van deze klus een orde van grootte hoger lag dan alles wat AI tot nu toe had geformaliseerd. In februari van dit jaar zette AI al een eerdere mijlpaal neer door het werk van wiskundige Maryna Viazovska over het optimaal stapelen van bollen in acht en 24 dimensies te controleren. Volgens Daniel Litt van de University of Toronto laat het Fermat-resultaat zien dat AI vrijwel elk wiskundig bewijs zou kunnen formaliseren, hoe ingewikkeld ook.

Meer dan een rekenkunstje

Het bewijzen van Fermats laatste stelling heeft op zichzelf weinig praktisch nut: niemand heeft iets aan de wetenschap dat deze vergelijking geen oplossingen heeft. De waarde zit in de technieken die Wiles ontwikkelde. Hij bewees onder meer de modulariteitsstelling, die elliptische krommen verbindt met modulaire vormen, en dat leverde uiteindelijk de sleutel tot het bewijs. Wiles ontving voor zijn werk in 2016 de Abelprijs, een van de meest prestigieuze onderscheidingen in de wiskunde. Dat AI nu in staat is zulk complex werk te controleren, betekent dat machines steeds vaker een rol gaan spelen bij het narekenen van wiskundig onderzoek. Sommige experts denken dat AI op termijn de hele bibliotheek van wiskundige kennis kan doorlichten, en zo bijvoorbeeld fouten kan blootleggen in resultaten die decennialang als waar golden. Twee jaar geleden noemde wiskundige Kevin Buzzard dat nog een fantasie.