Forskare samlades i London denna vecka för att påskynda formaliseringen av Fermats sista sats med hjälp av avancerade AI-modeller. Workshopen fokuserar på att konvertera Andrew Wiles bevis från 1993 till Lean-kod för datorverifiering. Framstegen har gått snabbt, med en fördubbling av kodrader efter den första dagen.
Tjugofem matematiker, datavetare och AI-experter möttes på ett hotell i centrala London för att arbeta med projektet som leds av Kevin Buzzard vid Imperial College London. Det femåriga arbetet, som finansierades 2024, syftar till att lägga till satsen i Mathlib-arkivet för formaliserad matematik.
Före workshopen fanns det 20 000 rader kod i projektet. Efter den första dagen hade summan nått 40 000. Buzzard noterade att AI-kapaciteten förbättrats kraftigt sedan december förra året, vilket gör det möjligt för teamet att ta sig an mer av den underliggande matematiken än vad som ursprungligen planerats.
Hang Lu Su, även hon vid Imperial College London, beskrev processen som en industrialisering av intellektuellt arbete. Deltagarna använder modeller som Claude för att generera och förfina kod, även om farhågor kvarstår kring ordrikedom och den långsiktiga underhållbarheten av AI-genererat resultat.
Buzzard uttryckte tillförsikt om att de ursprungliga målen kommer att uppnås innan projektets slut. Hur långt teamet kommer i den fullständiga pyramiden av stödjande satser beror på framtida utveckling inom AI.