AI helpt Fermats laatste stelling te formaliseren

Wiskundigen aan Imperial College London hebben deze week AI ingezet op een van de lastigste bewijzen uit de moderne wiskunde: Fermats laatste stelling. Tijdens een workshop testten ze of taalmodellen stukken van dat bewijs kunnen omzetten in machineleesbare, formeel controleerbare code. New Scientist berichtte er op 10 juli over. Het gaat niet om een AI die zelf de stelling bewijst, maar om iets subtielers: het vertalen van menselijke wiskunde naar taal die een computer sluitend kan verifiëren.

Wat autoformalisatie precies is

Een formeel bewijs wordt geschreven in een bewijsassistent zoals Lean, waarin elke stap logisch waterdicht moet zijn. Dat handmatig doen kost enorm veel tijd. Autoformalisatie laat een AI die vertaalslag maken, waarna Lean controleert of er geen gaten in zitten. De controle blijft dus bij de machine, niet bij het taalmodel. Een fout in de vertaling wordt door de verificatie gewoon afgekeurd, wat het risico op verzonnen tussenstappen sterk beperkt.

Het project rond Fermats laatste stelling loopt al langer. Kevin Buzzard leidt aan Imperial College een meerjarig initiatief om het volledige bewijs in Lean te formaliseren, gefinancierd tot 2029. De moeilijkheid zit in de bagage: elliptische krommen, modulaire vormen en Galois-representaties zijn grotendeels nog niet in de standaardbibliotheken aanwezig.

Wat AI hierin al aankan

De cijfers van het bedrijf Math Inc geven een idee van het tempo. Met hun agent Gauss formaliseerde het team de sterke priemgetalstelling in 25.000 regels Lean, in drie weken. Een eerder handmatig project onder leiding van wiskundigen Terence Tao en Alex Kontorovich was daar achttien maanden mee bezig. In februari 2026 verifieerde Gauss de optimaliteit van sphere packing in dimensie 8 en 24, goed voor 200.000 regels code, opnieuw in ongeveer drie weken.

Toch is Fermat een ander kaliber. Buzzard verwacht dat delen waar alle definities al klaarstaan geschikt zijn voor AI, terwijl de definitie-zware stukken juist slecht gaan. Science News wees er eerder op dat deze aanpak de manier waarop wiskundigen bewijzen controleren fundamenteel kan veranderen, omdat een geverifieerd bewijs geen menselijke naleescontrole meer nodig heeft.

AI schuift op naar de exacte wetenschap

De tijdlijn past in een bredere beweging. Anthropic bouwt met Claude Science een werkomgeving voor onderzoekers, Meta liet zien dat het zinnen uit hersenactiviteit kan reconstrueren, en de nieuwste redeneermodellen presteren steeds beter op wiskundige taken. Dat laatste blijft lastig te meten, zoals de discussie rond benchmarkclaims van Meta aantoont. Formele verificatie biedt daar een hard alternatief: een bewijs klopt of het klopt niet.

Wat betekent dit

Voor wiskundigen verschuift het werk van zelf elke stap uitschrijven naar het aansturen en controleren van een AI die het zware vertaalwerk doet. Voor de rest van de sector is het een teken dat modellen die je kent van kantoortoepassingen als Copilot ook in de exacte wetenschap voet aan de grond krijgen. Of Fermats laatste stelling binnen enkele jaren volledig in Lean staat, is nog onzeker. Dat AI het proces meetbaar versnelt, is dat inmiddels niet meer.