Claude formalitza l'últim teorema de Fermat: la primera demostració completa verificada per ordinador

Què s'ha anunciat exactament

Anthropic va publicar el 4 de setembre de 2026 una pàgina de recerca, un post de blog i un repositori obert a GitHub amb la formalització completa de l'últim teorema de Fermat en Lean 4. El teorema en si fa temps que està demostrat, des del 1995, quan Andrew Wiles va tancar un enunciat que havia resistit 358 anys. La novetat no és el resultat matemàtic, sinó que per primera vegada la demostració sencera està escrita en un llenguatge que un programa pot comprovar pas a pas, sense deixar res a la interpretació del lector.

L'últim teorema de Fermat afirma una cosa que s'explica en una línia: l'equació x elevat a n més y elevat a n igual a z elevat a n no té solucions amb nombres enters positius quan n és més gran que 2. Per a n igual a 2 hi ha solucions de sobres (3, 4 i 5, per exemple). A partir d'aquí, cap. Aquesta simplicitat aparent és la que va convertir el problema en una obsessió durant tres segles i mig, i la que contrasta amb els centenars de pàgines de matemàtiques avançades que van caldre per tancar-lo.

Què vol dir formalitzar una demostració

Una formalització consisteix a traduir una demostració escrita en el llenguatge habitual dels matemàtics —prosa, notació i una bona dosi de passos que es donen per evidents— al llenguatge d'un assistent de proves, un programa que verifica mecànicament cada inferència. Lean 4 és un d'aquests assistents: si accepta un teorema, és perquè ha comprovat que es dedueix dels axiomes de partida sense cap salt. El teorema formalitzat, és a dir verificat pas a pas per un programa, ofereix una garantia de correcció que cap revisió humana no pot igualar.

La formalització de Claude es basa en Mathlib, la biblioteca comunitària de matemàtiques de Lean 4, i utilitza únicament els tres axiomes estàndard del sistema. Tampoc no conté cap sorry, la instrucció amb què Lean permet deixar un forat pendent de demostrar: si n'hi hagués un de sol, l'edifici no s'aguantaria. Dos verificadors externs independents, comparator i nanoda, van revisar el resultat.

Onze dies, agents en paral·lel i cap línia humana

El treball es va fer entre el 7 i el 17 d'agost de 2026 sobre Prove2Me, una plataforma desenvolupada pel grup de Tianyi Peng a la Universitat de Colúmbia. Diversos agents de Claude van treballar en paral·lel repartint-se tres funcions: escriure els enunciats dels teoremes intermedis, revisar-se aquests enunciats entre ells i demostrar-los. Els humans de l'equip d'Anthropic van aportar l'enunciat d'una línia del teorema objectiu i, de tant en tant, comentaris sobre què calia prioritzar o simples missatges d'ànim. Ni una línia de matemàtiques, ni una línia de Lean.

Les xifres donen la mesura de l'esforç: 29.511 teoremes en l'arbre final del qual depèn l'enunciat principal i uns 30.300 de demostrats en total a la plataforma, amb uns 533.000 lemes de suport locals repartits pels fitxers. En conjunt, uns 13 milions de línies de codi Lean, que baixen a uns 10,5 milions si es descompta el boilerplate (codi repetitiu generat automàticament). Cent sis fitxers es van adaptar, amb crèdit, del projecte de formalització de Fermat de l'Imperial College London i del projecte flt-regular.

Aquest projecte de l'Imperial College, finançat per l'EPSRC (el consell britànic de recerca en enginyeria i ciències físiques), fa anys que treballa en la mateixa fita amb equips humans. Claude no va partir de zero: es va basar en el blueprint (pla detallat) que descompon la demostració en peces manejables. La ruta seguida és la clàssica de Wiles i Taylor-Wiles, tal com la van exposar Darmon, Diamond i Taylor: es construeix una corba de Frey a partir d'una hipotètica solució, s'invoca el teorema de Mazur, es passa per Langlands-Tunnell en el nombre primer 3, es canvia del nombre primer 3 al 5, s'aplica el pas d'elevació de modularitat conegut com a R=T i es remata amb el teorema de Ribet, que rebaixa el nivell fins a 2, on senzillament no existeixen les formes que caldrien. La contradicció tanca l'argument.

Per què importa i què no demostra

És l'exemple més ambiciós fins ara d'una intel·ligència artificial fent matemàtiques verificades de manera autònoma i sostinguda en el temps. No es tracta de resoldre un problema d'examen en segons, sinó de mantenir durant onze dies un projecte de milers de peces encaixades, amb diversos agents coordinant-se i corregint-se. Si aquesta capacitat es generalitza, la demostració formal deixa de ser un luxe reservat a resultats cèlebres i es converteix en una eina rutinària, primer en matemàtiques i a la llarga en programari crític, on un error verificable a temps val molts diners i de vegades vides.

També convé acotar-ne l'abast. La garantia que aporta Lean és de correcció lògica, no de comprensió: la màquina ha produït una cadena de deduccions que el verificador accepta, i el debat sobre si això equival a entendre les matemàtiques continua tan obert com abans. La mateixa Anthropic hi afegeix una cautela: no ha verificat de manera independent les afirmacions matemàtiques que apareixen als extractes del raonament de Claude inclosos en el seu document tècnic. El que s'ha verificat és el codi Lean; els comentaris sobre el que Claude es pensava que estava fent són una altra cosa.