Historias de la IA: ¿Será Lean el Katz 2.0 de la IA?
En estos momentos en los que la IA está probando resultados matemáticos de gran recorrido y relevancia, conviene recordar un aspecto clave en una demostración matemática: la comprobación de que es correcta.
Recordemos lo que ocurrió con una de las demostraciones más apasionantes de las matemáticas, el Teorema de Fermat por Andrew Wiles. Wiles anunció su prueba y el eco mediático y científico fue enorme, tal y como ha ocurrido ahora con el problema de Navier-Stokes. Pero una demostración de este nivel requiere el análisis cuidadoso de la comunidad y en este caso, Wiles se sirvió de uno de sus colegas, Nicholas Katz, como verificador.
Wiles llevaba siete años encerrado, sin que nadie supiera lo que estaba haciendo. A principios de 1993, para comprobar que no se había equivocado en la parte más delicada del argumento, organizó un curso de posgrado secreto en Princeton («Cálculos sobre curvas elípticas») al que asistía Katz; los estudiantes fueron abandonando y Katz acabó siendo el único oyente. Como no detectaron nada equivocado, Wiles finalizó su demostración en la primavera de 1993, se trasladó a Cambridge en junio e hizo público su resultado.
Envió su artículo de 200 páginas a Inventiones Mathematicae, que lo remitió a seis referees; uno de ellos fue precisamente Katz, y fue él quien encontró un fallo en los argumentos de Wiles. Wiles se recluyó de nuevo, primero en solitario y después con la ayuda de su antiguo alumno Richard Taylor, y unos 14 meses más tarde consiguió reparar la demostración.
En nuestros días han ido tomando cuerpo varios comprobadores digitales. Quizás el más popular entre los matemáticos sea Lean. Lean es un asistente de demostración y un lenguaje de programación funcional, basado en el llamado Cálculo de Construcciones Inductivas. Es importante decir que es un proyecto de software libre y de código abierto alojado en GitHub. Actualmente, su desarrollo cuenta con el apoyo de la organización sin ánimo de lucro Lean Focused Research Organization (FRO).
Entre los logros recientes de Lean, citemos que, en 2021, se utilizó Lean para verificar la parte central de una demostración de Peter Scholze (medallista Fields) en el ámbito de las matemáticas condensadas (el llamado Liquid Tensor Experiment, completado en 2022). En 2023, Terence Tao dirigió la formalización en Lean de la demostración de la conjetura polinómica de Freiman-Ruzsa que había obtenido junto con Gowers, Green y Manners, y, desde finales de 2025, varios problemas de Erdős se han resuelto con la ayuda de la IA y se han verificado formalmente con Lean.
Aunque los matemáticos tenemos colegas que intentan ayudarnos en la verificación de nuestras pruebas, como fieles émulos de Nicholas Katz, será seguramente con Lean con lo que acabaremos contrastando esos resultados. Ya se están formando grupos de trabajo para aprender a usarlo y para crear nuevas librerías que vayan fortaleciendo las ya existentes. Lo que sí quisiera dejar como moraleja de la historia es el inmenso trabajo que desarrolló Wiles en soledad, la necesidad de comprobación de los colegas, y compararlo con lo fácil que ahora resulta usar una IA. Por cierto, hace unos días mantuvimos un intenso debate sobre si un modelo de OpenAI, por ejemplo, sería capaz de probar el teorema de Fermat y Lean de comprobar la demostración. Adelanto que las opiniones fueron muy diversas.
_________________
Manuel de León (CSIC, Fundador del ICMAT, Real Academia de Ciencias, Real Academia Canaria de Ciencias, Real Academia Galega de Ciencias, Presidente del ICM2006 Madrid y miembro del Comité Ejecutivo de IMU (2007-2024) y del Comité Ejecutivo del ISC (2014-2018). Web: https://www.manueldeleon.es