{"id":151332,"date":"2026-09-26T17:00:59","date_gmt":"2026-09-26T16:00:59","guid":{"rendered":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/?p=151332"},"modified":"2026-09-26T17:00:59","modified_gmt":"2026-09-26T16:00:59","slug":"historias-de-la-ia-sera-lean-el-katz-2-0-de-la-ia","status":"publish","type":"post","link":"https:\/\/www.madrimasd.org\/blogs\/matematicas\/2026\/09\/26\/151332","title":{"rendered":"Historias de la IA: \u00bfSer\u00e1 Lean el Katz 2.0 de la IA?"},"content":{"rendered":"

En estos momentos en los que la IA est\u00e1 probando resultados matem\u00e1ticos de gran recorrido y relevancia, conviene recordar un aspecto clave en una demostraci\u00f3n matem\u00e1tica: la comprobaci\u00f3n de que es correcta.<\/p>\n

\"\"<\/a>
Andrew Wiles<\/figcaption><\/figure>\n

Recordemos lo que ocurri\u00f3 con una de las demostraciones m\u00e1s apasionantes de las matem\u00e1ticas, el Teorema de Fermat por Andrew Wiles. Wiles anunci\u00f3 su prueba y el eco medi\u00e1tico y cient\u00edfico fue enorme, tal y como ha ocurrido ahora con el problema de Navier-Stokes. Pero una demostraci\u00f3n de este nivel requiere el an\u00e1lisis cuidadoso de la comunidad y en este caso, Wiles se sirvi\u00f3 de uno de sus colegas, Nicholas Katz, como verificador.<\/p>\n

Wiles llevaba siete a\u00f1os encerrado, sin que nadie supiera lo que estaba haciendo. A principios de 1993, para comprobar que no se hab\u00eda equivocado en la parte m\u00e1s delicada del argumento, organiz\u00f3 un curso de posgrado secreto en Princeton (\u00abC\u00e1lculos sobre curvas el\u00edpticas\u00bb) al que asist\u00eda Katz; los estudiantes fueron abandonando y Katz acab\u00f3 siendo el \u00fanico oyente. Como no detectaron nada equivocado, Wiles finaliz\u00f3 su demostraci\u00f3n en la primavera de 1993, se traslad\u00f3 a Cambridge en junio e hizo p\u00fablico su resultado.<\/p>\n

\"\"<\/a>
Nicholas Katz<\/figcaption><\/figure>\n

Envi\u00f3 su art\u00edculo de 200 p\u00e1ginas a Inventiones Mathematicae, que lo remiti\u00f3 a seis referees; uno de ellos fue precisamente Katz, y fue \u00e9l quien encontr\u00f3 un fallo en los argumentos de Wiles. Wiles se recluy\u00f3 de nuevo, primero en solitario y despu\u00e9s con la ayuda de su antiguo alumno Richard Taylor, y unos 14 meses m\u00e1s tarde consigui\u00f3 reparar la demostraci\u00f3n.<\/p>\n

En nuestros d\u00edas han ido tomando cuerpo varios comprobadores digitales. Quiz\u00e1s el m\u00e1s popular entre los matem\u00e1ticos sea Lean. Lean es un asistente de demostraci\u00f3n y un lenguaje de programaci\u00f3n funcional, basado en el llamado C\u00e1lculo de Construcciones Inductivas. Es importante decir que es un proyecto de software libre y de c\u00f3digo abierto alojado en GitHub. Actualmente, su desarrollo cuenta con el apoyo de la organizaci\u00f3n sin \u00e1nimo de lucro Lean Focused Research Organization (FRO).<\/p>\n

\"\"<\/a><\/p>\n

Entre los logros recientes de Lean, citemos que, en 2021, se utiliz\u00f3 Lean para verificar la parte central de una demostraci\u00f3n de Peter Scholze (medallista Fields) en el \u00e1mbito de las matem\u00e1ticas condensadas (el llamado Liquid Tensor Experiment, completado en 2022). En 2023, Terence Tao dirigi\u00f3 la formalizaci\u00f3n en Lean de la demostraci\u00f3n de la conjetura polin\u00f3mica de Freiman-Ruzsa que hab\u00eda obtenido junto con Gowers, Green y Manners, y, desde finales de 2025, varios problemas de Erd\u0151s se han resuelto con la ayuda de la IA y se han verificado formalmente con Lean.<\/p>\n

Aunque los matem\u00e1ticos tenemos colegas que intentan ayudarnos en la verificaci\u00f3n de nuestras pruebas, como fieles \u00e9mulos de Nicholas Katz, ser\u00e1 seguramente con Lean con lo que acabaremos contrastando esos resultados. Ya se est\u00e1n formando grupos de trabajo para aprender a usarlo y para crear nuevas librer\u00edas que vayan fortaleciendo las ya existentes. Lo que s\u00ed quisiera dejar como moraleja de la historia es el inmenso trabajo que desarroll\u00f3 Wiles en soledad, la necesidad de comprobaci\u00f3n de los colegas, y compararlo con lo f\u00e1cil que ahora resulta usar una IA. Por cierto, hace unos d\u00edas mantuvimos un intenso debate sobre si un modelo de OpenAI, por ejemplo, ser\u00eda capaz de probar el teorema de Fermat y Lean de comprobar la demostraci\u00f3n. Adelanto que las opiniones fueron muy diversas.<\/p>\n

_________________<\/p>\n

Manuel de Le\u00f3n<\/strong> (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\u00e9 Ejecutivo de IMU (2007-2024) y del Comit\u00e9 Ejecutivo del ISC (2014-2018). Web: https:\/\/www.manueldeleon.es<\/p>\n","protected":false},"excerpt":{"rendered":"

En estos momentos en los que la IA est\u00e1 probando resultados matem\u00e1ticos de gran recorrido y relevancia, conviene recordar un aspecto clave en una demostraci\u00f3n matem\u00e1tica: la comprobaci\u00f3n de que es correcta. Recordemos lo que ocurri\u00f3 con una de las demostraciones m\u00e1s apasionantes de las matem\u00e1ticas, el Teorema de Fermat por Andrew Wiles. Wiles anunci\u00f3 su prueba y el eco medi\u00e1tico y cient\u00edfico fue enorme, tal y como ha ocurrido ahora con el problema de Navier-Stokes. Pero una demostraci\u00f3n de este nivel requiere el an\u00e1lisis cuidadoso de la comunidad y en este caso, Wiles se sirvi\u00f3 de uno de sus\u2026<\/p>\n","protected":false},"author":49,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"ngg_post_thumbnail":0},"categories":[1],"tags":[49741,49639,49743,49742,33664],"blocksy_meta":{"styles_descriptor":{"styles":{"desktop":"","tablet":"","mobile":""},"google_fonts":[],"version":4}},"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t