L'últim teorema de Fermat —que no existeixen enters positius a, b i c que compleixin aⁿ + bⁿ = cⁿ per a cap n més gran que 2— va quedar demostrat matemàticament per Andrew Wiles el 1994, després de gairebé quatre segles com a conjectura. Convertir aquella demostració en un text que un ordinador pugui verificar línia a línia, sense donar per bons cap dels passos intermedis que un matemàtic humà assumeix implícits, és una tasca diferent: exigeix escriure-la sencera en un llenguatge formal com Lean, i fins ara ningú l'havia completat.
Anthropic ha anunciat el 4 de setembre que el seu model Claude ho ha aconseguit treballant de manera pràcticament autònoma durant onze dies a través de Prove2Me, una plataforma de formalització col·laborativa dissenyada per l'investigador Tianyi Peng i el seu equip a la Universitat de Columbia, que manté un mapa de teoremes pendents i coordina diversos agents de Claude perquè hi treballin en paral·lel. El procés ha generat 13 milions de línies de codi en Lean, ha demostrat 30.300 teoremes intermedis —29.500 dels quals s'utilitzen a la demostració final— i ha consumit uns sis mil milions de tokens de sortida d'un model de recerca intern d'Anthropic. La intervenció humana s'ha limitat a indicacions puntuals d'alt nivell de Peng, com assenyalar quin teorema convenia prioritzar.
La notícia és rellevant perquè és un dels casos més ambiciosos fins ara d'un sistema d'IA treballant de manera sostinguda i pràcticament sense supervisió humana directa en un projecte de matemàtiques pures, i perquè demostra que la verificació formal a gran escala —fins fa poc reservada a equips de matemàtics dedicant-hi anys— es pot completar en qüestió de dies quan es combina amb infraestructura pensada específicament per coordinar agents d'IA. L'últim teorema de Fermat era, a més, un dels reptes de formalització més coneguts encara pendents dins la comunitat de verificació formal.
Anthropic mateix matisa l'abast de la fita: Claude ha formalitzat una demostració ja existent, la de Wiles, no n'ha generat una de nova ni ha produït matemàtiques originals, i la mateixa empresa reconeix que el text resultant, de 13 milions de línies, és «probablement molt més llarg del que caldria», lluny de la concisió que té la biblioteca de referència Mathlib. Aproximadament un 7% de les línies no trivials del resultat final provenen d'intents fallits inicials que calia descartar, i el projecte ha consumit una quantitat de còmput considerable per a un sol resultat matemàtic.