En lo que especialistas describen como un hito de proporciones históricas para la ciencia, la empresa tecnológica Anthropic anunció que su inteligencia artificial ha conseguido «formalizar» de extremo a extremo el último teorema de Fermat, verificando por completo su demostración mediante computadora en apenas once días de cómputo autónomo.
El sistema generó 13 millones de líneas de código y demostró 29.500 teoremas intermedios para verificar por computadora el histórico enigma matemático
Planteado por el matemático francés Pierre de Fermat en 1637, el enigma postula que no existen números enteros positivos que satisfagan la ecuación aⁿ + bⁿ = cⁿ cuando n es mayor que 2. La humanidad tardó casi 360 años en hallar una prueba concluyente, lograda por el británico Sir Andrew Wiles en 1995 tras un manuscrito de 129 páginas que requirió meses de revisión extenuante por parte de la comunidad académica internacional.
Para garantizar que una demostración sea matemáticamente infalible y comprensible para máquinas, los investigadores recurren a la «formalización» en lenguajes especializados como Lean. A través de un entramado de decenas de agentes inteligentes de Claude coordinados con la plataforma Prove2Me, el sistema redactó más de 13 millones de líneas de código Lean y demostró de forma sucesiva 29.500 lemas y teoremas intermedios, consumiendo aproximadamente seis mil millones de tokens en un modelo avanzado de investigación interna.
Kevin Buzzard, eminente matemático del Imperial College de Londres que lideraba una iniciativa colectiva desde 2024 para formalizar manualmente la obra de Wiles, calificó el resultado de «extraordinaria proeza». El catedrático subrayó que estas capacidades de auto-formalización permitirán auditar y erradicar inconsistencias en la literatura científica global, al tiempo que aliviarán la carga de revisión que enfrentan los evaluadores humanos ante la creciente producción de descubrimientos asistidos por computadora.
