Claude reescribió el teorema de Fermat
La empresa Anthropic afirmó que su sistema de inteligencia artificial Claude había creado una versión completamente verificable por ordenador de la demostración del último teorema de Fermat, uno de los problemas más conocidos de la historia de las matemáticas.
La conjetura fue formulada por el matemático francés Pierre de Fermat en 1637. Afirma que, para números enteros positivos, la ecuación xⁿ + yⁿ = zⁿ no tiene soluciones si n es mayor que 2. El matemático británico Andrew Wiles publicó la demostración completa en 1995; la versión matemática convencional ocupaba 129 páginas.
Anthropic no ha descubierto de nuevo el teorema. La empresa ha traducido una demostración ya existente a un formato formal; es decir, ha plasmado los razonamientos matemáticos como código que un programa especializado puede verificar automáticamente, paso a paso y sin depender de la intuición humana.
Las estimaciones iniciales apuntaban a que ese trabajo llevaría varios años. Sin embargo, según Anthropic, una versión interna de investigación de Claude necesitó 11 días de trabajo ininterrumpido y en gran medida autónomo. Las personas daban indicaciones generales al sistema, pero no se dedicaban a escribir código a mano de forma continua.
El resultado final consta de unos 13 millones de líneas de código especializado en Lean, un lenguaje que utilizan los matemáticos para formalizar demostraciones. Es más de cinco veces el tamaño de Mathlib, la principal biblioteca pública de demostraciones matemáticas formalizadas.
Durante el proceso, los agentes de Claude demostraron, según se ha informado, unas 30.300 proposiciones independientes, de las que alrededor de 29.500 se incluyeron en la versión final. Estos resultados intermedios abarcaron álgebra, análisis armónico, geometría y teoría de números. También contribuyeron varios intentos fallidos anteriores: representaron aproximadamente el 7 % de las líneas del texto final que no eran código estándar de plantilla.
El matemático Kevin Buzzard, del Imperial College de Londres, calificó el logro de extraordinario. A su juicio, el sistema demostró el último teorema de Fermat basándose únicamente en axiomas matemáticos, y las construcciones formales creadas ya son lo bastante fiables como para servir de base a futuros trabajos.
El nuevo resultado llega aproximadamente un mes después de que Anthropic informara de otro proyecto relacionado con la función zeta de Riemann. Esta función ocupa un lugar central en la hipótesis de Riemann, uno de los problemas sin resolver más difíciles de las matemáticas actuales.
OpenAI también trabaja en una línea parecida: el laboratorio utiliza el modelo Astra para resolver problemas clásicos asociados al matemático Pál Erdős. Se informó de que ese trabajo también había ayudado a acotar varias cuestiones pendientes de larga data en informática teórica.
Según Anthropic, un factor decisivo fue que Claude tuviera acceso a Prove2Me, una herramienta de programación abierta creada por colaboradores externos. Ayuda a la IA a elegir el siguiente paso útil en un proceso de investigación largo y, al mismo tiempo, reduce el coste computacional del trabajo del modelo.
Anthropic ha ampliado el acceso gratuito y los créditos de investigación para los matemáticos que formalizan demostraciones, y también ha ofrecido subvenciones específicas de gran cuantía. Pero aún es pronto para celebrar la victoria total de las máquinas sobre los matemáticos: incluso a esta velocidad, formalizar un gran teorema llevó 11 días y 13 millones de líneas de código. Parece que la humanidad aún no se ha librado del trabajo; solo le han añadido un becario digital muy parlanchín.
PEREC.RU
Anthropic anunció la formalización del último teorema de Fermat mediante una versión interna de su IA Claude. Formalizar significa traducir una demostración matemática convencional a código que el sistema Lean pueda verificar automáticamente paso a paso. No es una nueva demostración del teorema, sino una reconstrucción informática del trabajo ya conocido del matemático británico Andrew Wiles, que publicó la demostración completa en 1995.
El último teorema de Fermat fue formulado por el matemático francés Pierre de Fermat en 1637. Afirma que la ecuación xⁿ + yⁿ = zⁿ no tiene soluciones en números enteros positivos si el exponente n es mayor que 2. La demostración de Wiles ocupaba 129 páginas en notación matemática convencional.
Anthropic esperaba que traducir la demostración a código formal llevara varios años. Según la empresa, Claude realizó el grueso del trabajo en 11 días de actividad ininterrumpida y en gran medida autónoma. La participación humana se limitó a indicaciones generales, sin escribir código a mano de forma continua.
La versión final contiene unos 13 millones de líneas de código en Lean. Es más de cinco veces el tamaño de Mathlib, la principal biblioteca pública de demostraciones matemáticas formalizadas. Durante el proyecto, los agentes de Claude demostraron aproximadamente 30.300 proposiciones independientes, de las que unas 29.500 se incorporaron a la versión definitiva. Se aprovecharon resultados de álgebra, análisis armónico, geometría y teoría de números. También contribuyeron los intentos previos de formalización: supusieron aproximadamente el 7 % de las líneas no estándar del código final.
El matemático Kevin Buzzard, del Imperial College de Londres, calificó el resultado de extraordinario y señaló que la demostración se basa únicamente en axiomas matemáticos. También afirmó que las construcciones formales obtenidas son lo bastante fiables para seguir trabajando a partir de ellas.
El proyecto forma parte de una carrera más amplia entre laboratorios de IA para automatizar la investigación matemática. Aproximadamente un mes antes, Anthropic había hablado de un trabajo relacionado con la función zeta de Riemann y la hipótesis homónima, uno de los problemas sin resolver más conocidos. OpenAI utiliza el modelo Astra para estudiar problemas clásicos de Pál Erdős y, según se ha informado, ha acotado varias cuestiones abiertas de informática teórica.
Anthropic atribuye el éxito al acceso de Claude a la herramienta abierta Prove2Me, creada por colaboradores externos. El programa ayuda a la IA a elegir el siguiente paso más útil en un trabajo de varias etapas y reduce los costes computacionales. La empresa también ha ampliado el acceso gratuito, los créditos de investigación y las ayudas para los matemáticos que se dedican a formalizar demostraciones.
La conclusión tiene dos caras. La IA acelera de forma notable la traducción de demostraciones complejas a un formato verificable por máquinas, pero el proceso sigue requiriendo mucho trabajo. Once días es una rapidez récord frente a las estimaciones iniciales, aunque el resultado sigue midiéndose en 13 millones de líneas de código especializado.
