Claude escribe en Lean una prueba verificada de Fermat
Anthropic reportó el 4 de septiembre de 2026 que Claude produjo la primera prueba completa verificada por computadora del Último Teorema de Fermat: unas 13 millones de líneas de Lean y unas 29.500 teoremas intermedios en unos 11 días de trabajo multiagente mayormente autónomo en la plataforma Prove2Me, usando los tres axiomas estándar de Lean y un enunciado alineado con el FLT de Mathlib. El investigador Tianyi Peng de Anthropic dirigió prioridades de alto nivel; Kevin Buzzard revisó el resultado y llamó extraordinaria la autoformalización, y dijo que técnicas así pueden ayudar a chequear matemática generada por IA y aliviar el refereeing. Anthropic lo enmarca como verificación del camino de Wiles (vía Darmon–Diamond–Taylor), no matemática nueva como un resultado de Riemann, ni un lanzamiento de producto Claude para consumidores.
This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics.