Inteligencia artificial completa la primera demostración verificada por computadora del último teorema de Fermat

Hace casi 350 años, el matemático francés Pierre de Fermat escribió en el margen de un libro de Diofanto una afirmación que se convertiría en una de las conjeturas más famosas de la historia: no existen enteros positivos a, b y c que satisfagan la ecuación aⁿ + bⁿ = cⁿ cuando n es mayor que 2. El llamado último teorema de Fermat resultó ser increíblemente difícil de demostrar.

La primera demostración correcta llegó en 1995, obra del matemático británico Andrew Wiles. Su prueba ocupaba 129 páginas y requirió meses de trabajo minucioso para verificar. Sin embargo, hasta hace poco, ninguna demostración había sido verificada completamente por una computadora.

Ahora, un equipo de Anthropic anunció un hito histórico: su modelo de inteligencia artificial llamado Claude logró completar la primera demostración integral y verificada por computadora del último teorema de Fermat. El tiempo que tomó: apenas 11 días, cuando los expertos calculaban que un proyecto así necesitaría una década de trabajo humano.

“El hecho de que una máquina pudiera transformar el trabajo de matemáticos humanos en una demostración de 13 millones de líneas de código, completamente impecable, simplemente me dejó boquiabierto”, expresó Alex Kontorovich, matemático especializado en teoría de números de la Universidad de Rutgers en Nueva Jersey.

La demostración formalizada por IA sigue una versión simplificada de la prueba de Wiles desarrollada por Darmon, Diamond y Taylor. Durante el proceso, Claude escribió 13 millones de líneas de código en el lenguaje de programación Lean y demostró 29.500 teoremas intermedios. Para dimensionar la magnitud del logro, el código de la demostración es más de cinco veces mayor que Mathlib, la principal biblioteca comunitaria de demostraciones matemáticas.

Kevin Buzzard, matemático del Imperial College de Londres que lideraba un esfuerzo comunitario desde 2024 para completar esta formalización, calificó el resultado como “extraordinario”. Señaló que la prueba funciona sin más supuestos que los axiomas de las matemáticas, y que a lo largo del proceso se logró la formalización de álgebra, análisis armónico, geometría y teoría de números.

El matemático Daniel Litt, de la Universidad de Toronto, concordó en que si pueden formalizar el último teorema de Fermat, probablemente pueden formalizar cualquier cosa.

Más allá de la proeza técnica, el logro tiene implicaciones profundas para el futuro de las matemáticas. A medida que la inteligencia artificial produzca cada vez más demostraciones, la capacidad de formalizar fácilmente el trabajo podrá aliviar la carga de evaluar nuevos resultados, un proceso que actualmente puede tomar años. Los expertos señalan que en dos años esto habría sido considerado una fantasía, pero ahora es una realidad que podría permitir pronto a las máquinas examinar toda la biblioteca del conocimiento matemático, quizás descubriendo que algunos resultados ampliamente aceptados contienen errores.

El último teorema de Fermat, propuesto en 1637, permaneció sin demostrar durante más de tres siglos y medio. La demostración de Wiles de 1994 fue reconocida como uno de los logros matemáticos más importantes del siglo XX y le mereció el Premio Abel en 2016.