Una demostración que una máquina puede comprobar
Anthropic anunció el 4 de septiembre que un modelo interno de investigación ha producido la primera demostración del último teorema de Fermat verificable de principio a fin por ordenador. La formalización ocupa unos 13 millones de líneas de Lean, el asistente de demostración que los matemáticos usan para obligar a que cada paso de un argumento adopte una forma que una máquina pueda comprobar. Anthropic afirma que el trabajo llevó 11 días.
El último teorema de Fermat sostiene que ningún trío de enteros positivos satisface a^n + b^n = c^n para ningún entero n mayor que dos. Andrew Wiles lo demostró en 1995 en un artículo de unas 129 páginas, apoyado en maquinaria construida a lo largo del siglo XX. Revisar a mano una demostración así lleva años a los especialistas. Formalizarla se esperaba que llevara un plazo comparable.
Qué hizo realmente el modelo
Según Anthropic, el sistema era un modelo interno de propósito general, aproximadamente equiparable a Claude Fable 5.1, y no un motor matemático a medida. La empresa afirma que varias decenas de agentes trabajaron en paralelo, generaron unos seis mil millones de tokens de salida y demostraron 30.300 teoremas, de los cuales 29.500 aparecen en el resultado final. La intervención humana se limitó a orientación de alto nivel.
Anthropic señala que los primeros intentos fracasaron por completo. La ejecución que funcionó dependió de una plataforma interna que la empresa llama Prove2Me, que registra qué teoremas dependen de cuáles y permite que muchos agentes trabajen en ramas distintas de la misma demostración sin perder el hilo. Alrededor del siete por ciento de las líneas no rutinarias del archivo final proceden de los intentos fallidos.
El trabajo humano que hay debajo
El resultado no surge de la nada. Sigue una versión simplificada del argumento de Wiles expuesta por Henri Darmon, Fred Diamond y Richard Taylor, y se apoya en Mathlib, la biblioteca matemática comunitaria que miles de colaboradores han construido en Lean durante más de una década, y en el proyecto de formalización que dirige Kevin Buzzard en el Imperial College de Londres. Buzzard, que revisó el resultado, resumió su importancia en términos de fiabilidad: los artefactos, dijo, ya son lo bastante sólidos como para construir sobre ellos.
La propia Anthropic señaló límites. La demostración se apoya únicamente en los tres axiomas estándar de Lean, y un comparador confirmó que el enunciado demostrado coincide con la formulación del teorema en Mathlib — la comprobación que evita que un sistema demuestre algo sutilmente más débil de lo que afirma. Pero la empresa también reconoce que la demostración es probablemente mucho más larga de lo necesario, lo que importa a quien quiera reutilizar sus piezas.
Por qué lo interesante es la formalización
Las matemáticas arrastran desde hace décadas un cuello de botella de verificación: las demostraciones de frontera son tan largas que solo un puñado de personas puede revisarlas, y algunos errores han sobrevivido a la publicación. La formalización elimina el problema del revisor, a cambio de una cantidad enorme de trabajo tedioso. Ese intercambio la ha mantenido como algo poco frecuente.
Si la mitad tediosa puede automatizarse a esta escala, el cálculo cambia. Además se suma a una serie de anuncios parecidos: Anthropic publicó en agosto un trabajo sobre resultados nuevos de Claude en torno a la función zeta de Riemann, y OpenAI ha afirmado que su modelo Astra resolvió varios problemas abiertos de Erdős.
Lo que conviene vigilar es la reutilización independiente. Un archivo de 13 millones de líneas en Lean es verificable por construcción — para eso sirve Lean — pero su valor para los matemáticos en activo depende de si los teoremas intermedios pueden incorporarse a Mathlib y usarse en otros contextos. Anthropic no ha dicho cuándo, ni si, publicará el artefacto completo para ello.
