Cuando la IA «resuelve» una conjetura sin demostración: la respuesta de los matemáticos

Imagina que un modelo de IA anuncia haber resuelto una conjetura geométrica de hace ochenta años. No hay demostración publicada en una revista con revisión por pares, ni código fuente disponible, ni datos de entrenamiento divulgados. Solo un comunicado de prensa. Para un matemático, resulta aproximadamente tan convincente como un prestidigitador que afirmara haber descubierto la ley de la gravedad porque hace levitar un sombrero.

Es precisamente este tipo de situación —relatada por Ars Technica dos semanas después de que OpenAI anunciara un supuesto resultado matemático— lo que precipitó la redacción de un texto colectivo que se convirtió, en pocas semanas, en un acontecimiento para la comunidad matemática internacional. La Leiden Declaration on Artificial Intelligence and Mathematics, depositada el 2 de junio de 2026 con el DOI 10.5281/zenodo.20302944, no es un reglamento, ni una ley, ni un manifiesto antitecnológico. Es algo más raro: un texto normativo, redactado por investigadores para investigadores, en el preciso momento en que una disciplina advierte que las reglas del juego están cambiando sin que se la haya consultado.

Todo comenzó en septiembre de 2025, durante un taller en el Lorentz Center de Leiden titulado «Mechanization and Mathematical Research». Unos sesenta participantes de diez países —matemáticos, informáticos, historiadores y antropólogos de la ciencia— se reunieron para debatir qué le hace la automatización a su disciplina. De estos intercambios nació un grupo de trabajo convocado por Jim Portegies, de la Eindhoven University of Technology, que dedicó los seis meses siguientes a elaborar un texto común, según relata la Universidad de Leiden.

El resultado lleva la firma de dieciséis autores cuyas afiliaciones abarcan Washington, Edimburgo, Ámsterdam, Warwick, San Diego, Columbia, Cambridge, Oxford y Zúrich. Rodrigo Ochigame, historiador y antropólogo de la IA en Leiden University y coautor, resume la ambición: «Trabajamos en la declaración durante varios meses, reuniendo distintos puntos de vista en busca de principios compartidos.» Desde entonces, el texto ha recibido el respaldo de la International Mathematical Union, la organización internacional vinculada, entre otras cosas, a las medallas Fields y al Congreso Internacional de Matemáticos (ICM). Su secretario general, Christoph Sorger, quiso precisar: «La IMU respalda la Declaración de Leiden porque constituye una contribución oportuna, seria y equilibrada a un debate que no ha hecho más que empezar.» Y añadió: «Este respaldo no significa el final del debate.»

El texto identifica cinco valores fundamentales de la investigación matemática que el uso actual de la IA amenaza: la certeza de las demostraciones, la atribución verificable de los resultados, la transparencia de los argumentos, los estándares colectivos de evaluación y la autonomía de la disciplina frente a lógicas comerciales externas.

La primera amenaza es quizá la más técnica y la más insidiosa. «Las técnicas automatizadas actuales pueden producir argumentos plausibles, pero poco fiables, e incluso incorrectos, difíciles de distinguir de auténticas demostraciones matemáticas», advierte la declaración. El problema es evidente: una demostración matemática no es un texto que se parece a una demostración. Es un objeto lógico cuyos pasos deben poder verificarse. Un gran modelo de lenguaje puede encadenar símbolos con una fluidez impresionante y, sin embargo, cometer un error de razonamiento en la línea 47, un error que solo detectará un experto humano atento.

La distinción es fundamental. Como lo expresa Jeremy Avigad, profesor de Carnegie Mellon University, en su artículo sobre el giro formal en matemáticas: «Ahora podemos escribir definiciones, teoremas y demostraciones en lenguajes idealizados, semejantes a los lenguajes de programación, que los ordenadores pueden interpretar y verificar.» Pero verificar no es generar. Y ahí es precisamente donde los modelos de IA generativa plantean un problema: generan sin garantizar.

La segunda amenaza afecta a la atribución y a los derechos de autor. Matemáticos ven cómo sus artículos publicados en arXiv —de libre acceso, conforme a la tradición de apertura de la disciplina— se utilizan para entrenar modelos comerciales, sin consentimiento ni compensación. Ochigame lo formula sin rodeos: «Los matemáticos que nunca tuvieron intención de contribuir al desarrollo de la IA ven que su trabajo se utiliza con ese fin sin su consentimiento.»

La tercera amenaza, más difusa, es el hype, el bombo mediático. Michael Harris, matemático de Columbia University y coautor de la declaración, diagnostica el problema con precisión quirúrgica: «La industria tecnológica opera según una lógica comercial, antitética a los valores de las matemáticas.» Cuando una empresa anuncia un resultado matemático mediante un comunicado de prensa antes de que exista publicación verificable alguna, se salta el proceso de validación colectiva que lleva siglos siendo el núcleo de la práctica matemática.

Tras las cuestiones éticas se esconde una pregunta matemática e informática concreta. ¿Cómo saber que una demostración es correcta si no podemos verificarla nosotros mismos? La comunidad de los asistentes de demostración formales —programas como Lean o Coq— ha desarrollado desde la década de 1970 una respuesta elegante: el criterio de de Bruijn. Como explican Henk Barendregt y Freek Wiedijk en su artículo fundacional sobre el desafío de las matemáticas computacionales, un asistente de demostración satisface este criterio si la demostración producida puede comprobarse de forma independiente mediante un pequeño programa verificador, separado del sistema que ayudó a construirla. La confianza no descansa en la inteligencia del generador, sino en la transparencia del verificador.

Esto es exactamente lo que no proporcionan los modelos de IA propietarios. Cuando el modelo es inaccesible, como subraya Ochigame, «el modelo de IA es propietario y no está disponible para nadie fuera de la empresa», no puede aplicarse el criterio de de Bruijn. No hay verificación independiente. No hay demostración en el sentido matemático del término.

La biblioteca Mathlib, desarrollada para el asistente de demostración Lean y descrita en el artículo de la comunidad mathlib, ilustra la alternativa: un corpus comunitario de definiciones, teoremas y demostraciones verificadas que abarca álgebra, topología, teoría de categorías y análisis, construido de forma distribuida, sin autoridad central y de libre consulta. Es el modelo que la declaración defiende implícitamente: abierto, verificable y atribuible.

Las recomendaciones son precisas y operativas. Se invita a los investigadores a declarar explícitamente el uso de herramientas automatizadas —grandes modelos de lenguaje, asistentes de demostración y programas matemáticos— en una sección específica de sus artículos. La responsabilidad por la exactitud de los resultados sigue recayendo en los seres humanos. Los resultados no deben presentarse como producidos únicamente por una empresa o un modelo cuando intervienen contribuciones humanas y trabajos previos. Además, los autores deben poder negarse a que sus publicaciones se utilicen como datos de entrenamiento.

La declaración no pide prohibir la IA en matemáticas. Leslie Ann Goldberg, responsable de informática en la University of Oxford y firmante, formula con sobriedad el riesgo real: «Los borradores inexactos generados por IA son baratos de producir, y existe el riesgo de saturar la literatura con supuestos resultados que sencillamente son falsos.» El problema no es la herramienta. Es la ausencia de normas para utilizarla.

Peter Scholze, director del Max Planck Institute for Mathematics y medallista Fields, resume la cuestión filosófica: «El objetivo de la investigación matemática es la comprensión humana de las matemáticas; por tanto, las matemáticas solo pueden prosperar en una comunidad de investigadores humanos.» La propia declaración lo formula en una frase: «Las matemáticas son, y deben seguir siendo siempre, una empresa profundamente humana.»

Está prevista una sesión específica el 26 de julio de 2026 durante el ICM 2026, según anuncia IMU News de mayo de 2026. El debate no ha hecho más que empezar.

Para comprender con precisión qué está en juego, hay que distinguir tres niveles de relación entre la IA y la demostración matemática.

El primer nivel es la generación de texto matemático: un gran modelo de lenguaje produce en lenguaje natural un texto que se parece a una demostración. Es lo que hacen modelos como GPT-4 o Claude. El problema es que la plausibilidad textual y la validez lógica son dos cosas distintas. Un modelo puede alucinar un paso de razonamiento con la misma fluidez con que enuncia un lema correcto.

El segundo nivel es la verificación formal: una demostración se escribe en un lenguaje formal —Lean, Coq, Isabelle— que el asistente de demostración puede comprobar mecánicamente. Como mostraron Jeremy Avigad y John Harrison en su artículo publicado en Communications of the ACM, la verificación formal podría convertirse en un nuevo estándar de rigor en matemáticas. Aquí la confianza no descansa en la pericia del lector, sino en la lógica del verificador.

El tercer nivel, el más ambicioso, es la autoformalización: traducir automáticamente una demostración en lenguaje natural a un objeto formal verificable. El benchmark ProofNet, presentado en un artículo de Azerbayev, Piotrowski, Schoelkopf, Ayers, Radev y Avigad, contiene 371 ejemplos que asocian cada uno un enunciado formal en Lean 3, un enunciado en lenguaje natural y una demostración en lenguaje natural, extraídos de manuales universitarios de análisis real, álgebra lineal y topología. Resultado: en sus experimentos, el modelo Code-davinci-002 formalizaba correctamente el 13,4 % de los teoremas en modo few-shot (es decir, con algunos ejemplos proporcionados en el contexto) y el 16,1 % con recuperación de instrucciones similares. La tasa de verificación sintáctica (typecheck rate) alcanzaba el 45,2 % con recuperación de instrucciones, lo que significa que más de la mitad de las salidas producidas ni siquiera superaban la comprobación sintáctica de Lean, antes de plantear siquiera la cuestión de su validez matemática.

Estas cifras no son una acusación contra la IA en matemáticas. Simplemente muestran que el camino entre un «texto matemático convincente» y una «demostración verificada formalmente» sigue siendo largo, y que la Leiden Declaration hace bien en distinguir cuidadosamente ambas cosas.