El matemático Kevin Buzzard, del Imperial College de Londres, está entrenando a ordenadores para que demuestren uno de los problemas más famosos de la historia de las matemáticas: el último teorema de Fermat.

Resolver el problema no es lo importante. Ya existe una demostración aceptada, finalizada en 1998. Este trabajo es un intrincado laberinto matemático que ocupa unas 130 páginas repartidas en dos artículos. Abarca diversos campos matemáticos y unifica ideas abstractas que antes parecían tener poca relación entre sí. Conocer la demostración implica dominar una amplia gama de matemáticas. En el futuro, afirma Buzzard, un programa informático capaz de verificar algo tan extenso podrá ayudar a los matemáticos a encontrar, analizar y resolver una gran variedad de problemas.

Durante años, Buzzard y un grupo de matemáticos han trabajado en proyectos como este para formalizar las matemáticas. Históricamente, la formalización ha consistido en expresar ideas matemáticas con la mayor precisión posible, eliminando toda ambigüedad. Hoy en día, esto significa traducir definiciones y teoremas a código informático para que un programa especializado pueda verificar cada paso minucioso.

La formalización “es un nuevo paradigma para la redacción de demostraciones matemáticas que exige, en esencia, que quien las redacta sea mucho más riguroso de lo habitual”, afirma la matemática Emily Riehl, de la Universidad Johns Hopkins. “El ordenador no se encarga de rellenar los detalles”. Es la persona que redacta la demostración quien debe hacerlo.

Pero formalizar la demostración del último teorema de Fermat es solo la piedra angular de una visión aún mayor: construir una biblioteca digital de todas las matemáticas que permita a las computadoras ser asistentes útiles para los matemáticos.

Incluso hoy en día, la mayoría de los matemáticos escriben demostraciones que se basan en descripciones orales o escritas e intuición, herramientas tradicionales que hasta hace poco parecían fuera del alcance de las computadoras. Por ello, la formalización moderna ha sido durante mucho tiempo un campo especializado, ya que requiere expresar ideas matemáticas mediante código.

Ahora, el auge de la inteligencia artificial ha impulsado iniciativas, lideradas por empresas tecnológicas, para combinar grandes modelos de lenguaje con demostradores de teoremas y desarrollar sistemas capaces de autoformalización. En teoría, estos sistemas podrían llegar a realizar tareas que los humanos no pueden.

Se trata de un objetivo controvertido que preocupa a muchos matemáticos por cómo podría transformar la investigación y el progreso matemáticos. Lo que comenzó como una cuestión filosófica —¿Cuál es la máxima precisión posible en una demostración matemática?— se ha convertido ahora en una cuestión existencial: ¿La búsqueda de la precisión revolucionará el campo de las matemáticas?

“Estamos realmente en el umbral de un cambio”, afirma Patrick Shafto, matemático e informático de la Universidad de Rutgers en Newark, Nueva Jersey, y de DARPA, una agencia de investigación y desarrollo del Departamento de Defensa de Estados Unidos.

“Actualmente, las matemáticas se practican básicamente en una pizarra, como hace 100 años. Pero creo que en cinco años, es muy probable que todos los jóvenes matemáticos utilicen IA”, afirma Shafto. “Los avances en IA y su formalización tienen el potencial de resaltar los aspectos más interesantes de la condición humana y nuestra búsqueda de conocimiento”.

Mi asistente robot

Puede que la IA haya actuado como un acelerador de la formalización, pero la idea de usar una máquina para demostraciones matemáticas no es nueva. En 1956, investigadores de la corporación RAND presentaron un programa informático (al que llamaron "máquina de teoría lógica") que verificaba las demostraciones publicadas en Principia Mathematica, una serie de libros fundamentales de los matemáticos Bertrand Russell y Alfred North Whitehead.

«Me alegra saber que ahora se puede realizar Principia Mathematica con maquinaria», escribió Russell en una carta a Herbert Simon, uno de los investigadores responsables de la máquina pensante. «Ojalá Whitehead y yo hubiéramos conocido esta posibilidad antes de perder diez años haciéndolo a mano».

Aunque no es una práctica muy extendida, algunos matemáticos han utilizado programas informáticos llamados demostradores interactivos de teoremas en las últimas décadas para verificar demostraciones matemáticas existentes. En 1998, el matemático Thomas Hales anunció que él y su alumno Samuel Ferguson habían utilizado un ordenador para demostrar la conjetura de Kepler, una afirmación sobre la forma óptima de apilar esferas que fue planteada originalmente por Johannes Kepler en el siglo XVII.

La demostración encontró cierta resistencia por parte de otros matemáticos, quienes argumentaron que, debido a que la computadora había realizado tantos cálculos enormes y complejos que representaban todas las configuraciones posibles de esferas apiladas, los humanos no podían comprobar la exactitud de las respuestas y, por lo tanto, no podían verificar el razonamiento. Así pues, entre 2003 y 2014, Hales utilizó asistentes digitales para formalizar y verificar su propia demostración.

En febrero, combinando la IA con un demostrador de teoremas interactivo, la matemática ucraniana Maryna Viazovska y otros terminaron de formalizar las demostraciones de la conjetura de Kepler en ocho y 24 dimensiones, versiones digitales del trabajo que le había valido a Viazovska la Medalla Fields en 2022.

El viaje de Buzzard hacia la formalización comenzó en 2017 con una especie de crisis existencial matemática. Acababa de revisar un artículo para su publicación en una revista de matemáticas y, tras un largo intercambio con el autor del artículo, no pudo determinar si el argumento era riguroso.

Esa frustración lo llevó a reflexionar ampliamente sobre el estado de las matemáticas y su potencial. «Me sentí bastante descontento con la situación actual», comentó durante una charla en septiembre. Empezó a preguntarse: ¿Podría la tecnología eliminar la incertidumbre en la verificación matemática? Al fin y al cabo, los matemáticos no se dedican a este campo para comprobar los entresijos de otras demostraciones, sino para crear algo nuevo. Si la verificación pudiera delegarse a una máquina, ¿por qué no?

Buzzard comenzó a aprender a usar Lean, que es a la vez un lenguaje de programación y un demostrador de teoremas interactivo. Lean apareció por primera vez en 2013, ideado por Leo de Moura, un científico informático de Microsoft, quien lo diseñó para verificar argumentos matemáticos, especialmente en código informático. Lean es el mismo demostrador de teoremas que se utilizó para formalizar la demostración de Viazovska en febrero.

Cuanto más aprendía Buzzard, más se entusiasmaba. Empezó a ver la formalización como el acto de digitalizar las matemáticas, lo que a su vez modernizaría la forma en que los matemáticos utilizan las máquinas. Lo compara con la digitalización de la música. Cuando las compañías discográficas empezaron a vender CD, Buzzard cuenta que al principio desestimó la tecnología, pensando que era una forma de obligar a los oyentes a volver a comprar música que ya poseían. Luego se dio cuenta de que los CD permitían a la gente acceder, compartir e interactuar con la música de maneras antes inimaginables, un cambio que se vio amplificado por la llegada de los servicios de streaming.

«La digitalización de la música ha revolucionado por completo el mundo musical», afirma Buzzard. «Si digitalizamos las matemáticas, quizás en algún momento también las revolucionemos». Reflexionó sobre su propia formación y sobre cómo impartía matemáticas, y se dio cuenta de que la gente había estado aprendiendo la materia de la misma manera durante el último siglo. Era hora de modernizarse.

Y Buzzard decidió comenzar con una ecuación de siglos de antigüedad que, hasta hace poco, era el problema sin resolver más famoso de las matemáticas.

Un gran misterio en un margen minúsculo

Según cuenta la leyenda, alrededor de 1637, el matemático francés Pierre de Fermat escribió un problema y una nota en un ejemplar de Aritmética, obra del matemático griego Diofanto, del siglo III. El problema plantea la siguiente ecuación: a ⁿ + b ⁿ = c ⁿ . Si n = 2, sabemos que existen infinitas soluciones. Esto se debe a que, en ese caso, la ecuación se convierte en el teorema de Pitágoras, donde a, b y c corresponden a las longitudes de los lados de triángulos rectángulos.

Fermat afirmó que no existen números enteros para a, b y c que puedan resolver esta ecuación si n es mayor que 2. Junto al problema, Fermat escribió en latín: «Tengo una demostración verdaderamente maravillosa de esta proposición que este margen es demasiado estrecho para contener».

El hijo de Fermat descubrió el libro y la nota, pero no hasta después de la muerte de su padre. El teorema era fácil de enunciar, pero difícil de demostrar, y la prueba que Fermat no había encontrado desconcertó a los matemáticos durante siglos. Nadie halló jamás su argumento «verdaderamente maravilloso», y ningún matemático logró concebir una demostración que se le pareciera remotamente. Algunos dudan de su existencia o conjeturan que la demostración que Fermat tenía en mente era fundamentalmente errónea. Resulta tentador considerar la afirmación de Fermat como una broma pesada con consecuencias extraordinarias.

El matemático británico Andrew Wiles finalmente lo resolvió a finales del siglo XX y, posteriormente, colaboró ​​con el matemático Richard Taylor para perfeccionarlo. Su demostración empleó conceptos matemáticos complejos y de gran alcance que no existían en el siglo XVII, ideas que conectan campos matemáticos que antes parecían inconexos.

A lo largo de los siglos, al analizar el sencillo problema de Fermat, los matemáticos han logrado avances extraordinarios en numerosos campos, más allá de la teoría de números, el campo más estrechamente relacionado con el problema original. En uno de los avances más significativos, el matemático alemán Ernst Kummer demostró en 1847 que el teorema se cumplía para los números primos regulares, un subconjunto de los números primos. Lo hizo desarrollando ideas que sentaron las bases de un nuevo campo llamado teoría algebraica de números.

En 2023, con el apoyo del Consejo de Investigación de Ingeniería y Ciencias Físicas del Reino Unido, Buzzard inició su proyecto de formalización del último teorema de Fermat, en parte debido a la magnitud e importancia de la demostración, y en parte porque muchos de sus colegas del Imperial College de Londres estaban explorando ideas utilizadas en ella. Sabía que sería una tarea hercúlea y compleja codificar cada definición y lema —similar a un mini-teorema integrado en una demostración más extensa— que desempeña algún papel en el esquema general. Y el camino ha sido accidentado. «Estoy un poco desorganizado y he tenido algunos comienzos fallidos», comenta.

No trabaja solo. Al principio, dice Buzzard, unas 30 personas contribuían a su esfuerzo de formalización escribiendo código para Lean, todos nombres y rostros conocidos. Muchos más se han puesto en contacto con ideas o han intentado unirse al proyecto, dice, y poco más de 60 han visto verificadas y aceptadas sus contribuciones de código. Aun así, el proyecto se ha convertido en una colaboración interdisciplinaria de una magnitud que Buzzard jamás habría imaginado. Teóricos de números anónimos se ponen en contacto con él para aportar ideas, dice. El pasado agosto, cuenta, fue de acampada a un festival de música durante una semana y, al regresar, encontró 7000 mensajes sin leer sobre diversos aspectos de la demostración.

En enero, el proyecto alcanzó uno de sus primeros hitos importantes. «Demostramos que algo era finito», lo que allanó el camino para el siguiente paso, afirma Buzzard. Sin embargo, el esfuerzo requerido para lograr ese hito le ha hecho dudar de si terminarán en el plazo previsto de cinco años.

Según Buzzard, uno de los mayores desafíos es encontrar la manera de crear rápidamente la biblioteca de conocimientos matemáticos de Lean. Esto también representa un obstáculo para las aplicaciones de IA en matemáticas. «En todo este ámbito de la IA aplicada a las matemáticas, existe una terrible falta de conjuntos de datos interesantes», afirma.

En un proyecto independiente financiado por Renaissance Philanthropy, Buzzard y el matemático de Rutgers, Alex Kontorovich, están contribuyendo aún más a la biblioteca de Lean —y ampliando su aplicabilidad— mediante la formalización de problemas de una lista de teoremas recientes, particularmente complejos, que representan la vanguardia de las matemáticas en el siglo XXI.

Las implicaciones van mucho más allá de los proyectos de Buzzard. Un volumen cada vez mayor de conocimiento matemático podría permitir a los matemáticos en activo —si así lo desearan— encontrar fallos en nuevas demostraciones o determinar si ciertas conjeturas son válidas. Los revisores y editores que evalúan artículos para revistas podrían centrarse en las ideas principales de los trabajos presentados, en lugar de en los minuciosos detalles lógicos de la demostración.

“Eso lo cambia todo”, dice Riehl. “Las demostraciones son difíciles y los artículos ya son muy largos”. Los errores pueden pasar desapercibidos.

Un demostrador de teoremas con acceso a una sólida base de conocimientos matemáticos podría utilizarse para identificar errores y otras inconsistencias en las demostraciones matemáticas generadas por programas de IA. Al fin y al cabo, que una demostración sea correcta en un 95 % puede significar que no lo es en absoluto. «Una sola inconsistencia puede invalidar todo un argumento matemático, porque esa es la naturaleza de las matemáticas», afirma Buzzard.

Por ese motivo, las empresas tecnológicas han estado desarrollando programas que combinan herramientas de IA como Gemini de Google o ChatGPT de OpenAI con el rigor de verificación de datos de Lean. El gobierno estadounidense también lo ha hecho: a principios de 2025, DARPA lanzó un programa llamado Exponentiating Mathematics, o expMath, con el objetivo de utilizar la IA para acelerar el ritmo de los descubrimientos matemáticos, principalmente delegando las tareas más complejas de la construcción de una demostración.

Todos estos esfuerzos están directamente relacionados con una cuestión más controvertida y en rápida evolución a la que se enfrenta la matemática actual: averiguar cómo va a cambiar la IA este campo y si la irrupción de la IA en las matemáticas es algo positivo.

Un espectro creciente de la IA

Hasta ahora, el problema con los grandes modelos de lenguaje y las matemáticas ha sido principalmente de precisión. Siendo justos, los modelos de lenguaje como los que impulsan ChatGPT y Claude de Anthropic resuelven mejor los problemas matemáticos de lo que se esperaba, y han mejorado con cada nueva versión. Pero no son perfectos.

«Si le pides a ChatGPT que demuestre un teorema, te devuelve un texto», explica Riehl. Puede que suene bien, se vea bien y use la terminología correcta, añade. «Pero no hay nada en el diseño de los grandes modelos de lenguaje que garantice su corrección». Esto se debe a que están diseñados para responder a consultas mediante probabilidad y no priorizan la precisión. E incluso si tiene un 99 % de precisión, afirma, eso no es suficiente para una demostración matemática.

Sin embargo, cuando se combinan con un demostrador de teoremas como Lean, los LLM mejoran considerablemente.

En julio pasado, la empresa de IA Harmonic fue noticia después de que su programa Aristóteles, que utiliza Lean para verificar y perfeccionar su trabajo, obtuviera una puntuación lo suficientemente alta como para ganar la medalla de oro, el máximo galardón, en la Olimpiada Internacional de Matemáticas. Durante este evento de dos días, los participantes, todos menores de 20 años, resuelven seis problemas de extrema dificultad. Más de 600 concursantes humanos participaron en la edición de 2025, celebrada en Queensland, Australia; 72 obtuvieron al menos 35 de los 42 puntos posibles, consiguiendo así la medalla de oro. Además de Aristóteles, programas de IA utilizados por Google y OpenAI también lograron resultados de nivel de medalla de oro.

Algunos matemáticos no consideraron que los logros de la olimpiada demostraran algo significativo sobre la forma en que se hacen las matemáticas en la práctica. Pero pronto surgieron resultados más interesantes. En julio, Kontorovich, de Rutgers, y Terence Tao, matemático de la UCLA y ganador de la Medalla Fields, anunciaron que el progreso en su proyecto de 18 meses para formalizar el teorema de los números primos fuertes se había ralentizado. Sin embargo, en septiembre, una empresa llamada Math, Inc., financiada por una subvención del proyecto expMath de DARPA, anunció que había utilizado su programa, llamado Gauss, para completar la tarea en tan solo tres semanas.

Gauss combinó Lean con modelos de lenguaje de IA para formalizar automáticamente el resto de la demostración; es decir, el programa de IA tradujo definiciones y argumentos a Lean, que verificó la exactitud de todo el argumento. Más recientemente, en enero, investigadores informaron haber utilizado Aristóteles y GPT-5.2 para generar, formalizar y verificar una demostración de un problema planteado por el prolífico matemático húngaro Paul Erdős en 1975. Esta es la última de una serie reciente de demostraciones de problemas de Erdős que utilizaron IA de alguna manera.

Hasta ahora, Buzzard recibe con escepticismo avances como estos. En este momento, no hay límites, afirma. Y aunque Lean informa que el código generado por IA es preciso, puede que no represente realmente el teorema que el matemático creía estar demostrando.

Al mismo tiempo, Buzzard admite que el panorama podría cambiar rápidamente dada la velocidad del avance de la IA. Hasta ahora, no ha visto ningún avance en IA que le sea útil en su trabajo. Sin embargo, reconoce que es posible que en cinco años surja alguna herramienta que simplifique la formalización de la demostración del último teorema de Fermat. «Me pregunto si la autoformalización llegará al punto en que, simplemente, podrá absorber toda la literatura», comenta Buzzard.

Ayudar a los humanos

Muchos matemáticos predicen que los humanos siempre serán necesarios en matemáticas, pero debido al uso de la IA y la formalización, su papel podría cambiar drásticamente.

«El aspecto de resolución de problemas de las matemáticas prácticamente desaparecerá», afirma el matemático e informático Christian Szegedy, de Math, Inc. Anteriormente, participó en el desarrollo del programa AlphaProof de Google DeepMind y codirigió la empresa xAI, fundada por Elon Musk. Según Szegedy, la nueva función de los humanos en matemáticas será «orientar la exploración matemática hacia las áreas que realmente nos interesan», en lugar de enredarse en la lógica y los detalles de una demostración. Considera que el auge de la autoformalización impulsada por la IA es un camino hacia la creación de un asistente digital brillante.

Szegedy cree que el verdadero progreso se manifestará en la capacidad de la IA para razonar de maneras nuevas y creativas. Predice que los sistemas de IA alcanzarán una «inteligencia sobrehumana» en matemáticas —la capacidad de resolver problemas que los humanos no pueden— este año. Hasta ahora, eso no ha sucedido.

Szegedy también predice que, en algún momento, los modelos de IA serán mejores que los humanos para formalizar demostraciones, algo que no parece descabellado dado el rápido ritmo de desarrollo en 2025. Pronto, cree, los modelos podrán crear una demostración desde cero. «Y entonces, se acabó el juego». No cree que los humanos vayan a quedar fuera del juego; se refiere a que el papel esencial del matemático será puramente creativo, dependiendo de un colaborador de IA para resolver los detalles.

Shafto, de DARPA, quien dirige el proyecto expMath, considera que estos cambios brindan a los matemáticos más tiempo y espacio para reflexionar sobre ideas en lugar de detalles. «Si hablas con matemáticos, claro que demuestran cosas y quieren que sean correctas, pero no es a lo que se dedican la mayor parte del tiempo», afirma. «Hablan de ideas, de cómo se relacionan y de qué podría funcionar. Muchos estarían encantados de tener un estudiante o colaborador de confianza que les demostrara sus pequeños lemas».

Otros expertos en el campo, sin embargo, observan la inminente ola de IA con escepticismo y preocupación por el futuro. «Muchos de mis colegas no tienen ningún interés en ello», afirma el matemático Aravind Asok, de la Universidad del Sur de California en Los Ángeles.

En los últimos años, afirma Asok, las empresas de IA han reinterpretado el logro matemático como una herramienta de legitimación. Las matemáticas, según él, se convierten en un problema a resolver. Considera que esta idea es errónea y una completa incomprensión de lo que son las matemáticas. La insistencia en que las matemáticas pueden resolverse mediante modelos de IA, o en que el objetivo principal es la precisión, exige una visión limitada del campo.

Pero esta perspectiva ya se ha infiltrado en su aula: Asok afirma que ya no asigna tareas porque muchos de sus estudiantes de posgrado utilizan IA para generar respuestas. Eso contradice el propósito. «Necesitan esforzarse y comprometerse con el trabajo de una manera que realmente desarrolle su propia intuición», explica. Sin embargo, es mucho más rápido consultar a ChatGPT.

A Asok le preocupa que las conversaciones sobre IA y matemáticas se centren demasiado en la precisión. Si bien es importante, afirma, «cometer errores forma parte del aprendizaje». Añade que ha habido muchos errores que han contribuido al avance de la investigación matemática.

La formalización es una herramienta poderosa que podría impulsar las matemáticas hacia direcciones interesantes, pero Asok teme que si los estudiantes aprenden matemáticas como algo que se aplica a la IA, los matemáticos del futuro carecerán de la creatividad necesaria para descubrir fronteras verdaderamente nuevas. "Es como decir que solo hay una forma de hacer música o una sola forma de conversar", afirma.

Asok también teme que la IA pueda representar una amenaza para la profesión debido a la percepción que se tiene del progreso. Los matemáticos suelen depender de la financiación federal, afirma, y ​​si el gobierno estadounidense adopta la idea de que las empresas de IA ya han resuelto los problemas matemáticos, el apoyo a nuevos trabajos e ideas podría disminuir. La enseñanza de las matemáticas, añade, podría delegarse en agentes y programas de IA. «Creo que el estatus profesional de los matemáticos podría cambiar drásticamente».

Buzzard sostiene que, con o sin IA, la formalización puede contribuir a modernizar las matemáticas y la enseñanza de las matemáticas. Los matemáticos se beneficiarían de un demostrador de teoremas interactivo con acceso a información matemática verificada, no solo para comprobar su trabajo, sino también como banco de pruebas para nuevos trabajos generados por IA, en parte para distinguir el código deficiente de los avances genuinos.

“Solo quiero mejorar la vida de mis compañeros”, dice Buzzard. “No intento destruirlos. De hecho, intento ayudarlos”.

Citas

K. Buzzard y R. Taylor. Hacia una demostración concisa del último teorema de Fermat. Imperial College London Github . Publicado el 3 de abril de 2026.

TC Hales. Empaquetamientos de esferas I. arXiv:math/9811073 . Publicado el 11 de noviembre de 1998.

A. Wiles. Curvas elípticas modulares y el último teorema de Fermat . Anales de Matemáticas. Vol. 141, mayo de 1995, págs. 443-551. doi.org/10.2307/2118559.

N. Sothanaphan. Resolución del problema n.º 728 de Erdős: un análisis de la demostración concisa de Aristóteles. arXiv:2601.07421 .
Publicado el 12 de enero de 2026.

Por Stephen Ornes​

​Autor​