El 20 de julio de 2026, Kevin Buzzard, profesor de matemáticas en el Imperial College de Londres, escribió en su blog una frase tan directa como incómoda para sus colegas: los matemáticos humanos están siendo «superados por contraejemplos». La razón es que la IA ha derribado tres conjeturas matemáticas que llevaban décadas sin resolverse en solo dos meses — una de ellas había permanecido abierta durante casi un siglo.
El propio Buzzard comenta: «Tardé menos de cinco minutos en verificar un contraejemplo de geometría algebraica que llevaba 60 años sin resolverse. Descargué el código Lean en mi portátil, lo compilé, asentí y dije: ‘Sí, esto es efectivamente un contraejemplo’.»
Cinco minutos. Esa es la línea divisoria entre las matemáticas humanas y las matemáticas de la IA. Lo que me interesa explorar aquí es cuándo se trazó esa línea y qué significa realmente.
El contraejemplo: un cuchillo más afilado que una demostración
Primero, un concepto básico. En matemáticas, demostrar que una proposición es verdadera es muy difícil — hay que construir una argumentación tan rigurosa que ni un solo paso pueda fallar. Pero demostrar que una proposición es falsa es comparativamente «sencillo»: solo necesitas encontrar un contraejemplo, una construcción concreta que satisface todas las premisas pero no la conclusión.
Si alguien dice «todos los cisnes son blancos», no necesitas revisar cada cisne del planeta; basta con encontrar un cisne negro.
Un solo contraejemplo puede poner fin a toda una línea de investigación matemática. Y precisamente por eso, los contraejemplos han desempeñado un papel creativo en la historia de las matemáticas: revelan los límites de una teoría, obligan a los matemáticos a reexaminar sus supuestos, refinar definiciones y hacer avanzar la disciplina. En cierto sentido, los contraejemplos son el combustible del progreso matemático.
La IA está llevando esta técnica de «encontrar cisnes negros» a una escala inimaginable.
De mayo a julio de 2026: el triplete de la IA
He aquí lo que ha ocurrido en estos tres meses, en orden cronológico.
Primer golpe: la conjetura de las distancias unitarias de Erdős (1946-2026)
El legendario matemático Paul Erdős planteó este problema de geometría discreta en 1946. ChatGPT proporcionó una construcción como contraejemplo. La primera reacción de Buzzard fue preguntar: «¿Está verificado en Lean?» No lo estaba. Pero menos de una semana después, el medallista Fields Mike Freedman (ahora director científico de Logical Intelligence, una empresa de IA) envió un correo: su sistema ya había traducido automáticamente el argumento a código Lean.
Un mes después, Boris Alexeev de OpenAI completó el trabajo usando el nuevo modelo Sol, partiendo de los axiomas matemáticos para formalizar por completo todo el contraejemplo. Sol generó 1,2 millones de líneas de código Lean para lograrlo.
Para ponerlo en contexto: la biblioteca matemática central mathlib, que la comunidad Lean ha construido durante nueve años, tiene solo 2,3 millones de líneas. Lo que la IA generó en tres semanas supera la mitad de lo que los humanos han acumulado en nueve años. El comentario de Buzzard fue escueto: «El desarrollo matemático generado masivamente por IA ya es inevitable.»
Segundo golpe: el problema del esquema en grupos de Grothendieck (década de 1960-2026)
Grothendieck, uno de los matemáticos más grandes del siglo XX, planteó una pregunta hace 60 años: ¿todo esquema en grupos finito y libre de orden n está necesariamente aniquilado por n? Deligne demostró que sí en el caso conmutativo; el propio Grothendieck probó el caso en que el anillo base es reducido. Pero la conclusión completa quedó abierta.
Sol encontró un contraejemplo. Toda la demostración tiene solo 1076 líneas de código Lean. Buzzard tardó menos de cinco minutos en verificarla entera. Le sugirió al matemático Akhil Mathew que enviara el contraejemplo a la biblioteca matemática — y luego bromeó: «¿Y si pruebas ahora con la conjetura de Hodge?»
Tercer golpe: la conjetura Jacobiana (1939-2026)
Este es el más impactante de los tres. La conjetura Jacobiana es un problema inverso sobre aplicaciones polinómicas: si el determinante jacobiano de una aplicación polinómica es una constante no nula, ¿es la aplicación necesariamente invertible? La cuestión llevaba abierta desde 1939 y se consideraba una de las conjeturas más seductoras y tozudas de la geometría algebraica.
Esta vez el golpe lo asestó Claude Fable, de Anthropic. Encontró el contraejemplo durante la final de la Copa del Mundo de 2026. Al día siguiente, Terence Tao — uno de los matemáticos más respetados del mundo — publicó una entrada en su blog detallando la «digestión» del contenido matemático del contraejemplo.
Los cálculos de Tao revelaron que el contraejemplo es una aplicación polinómica de tres variables con grado máximo siete. Su determinante jacobiano es -2 — cumple la condición de constante no nula — pero la aplicación envía tres puntos de entrada distintos al mismo punto de salida, por lo que no es inyectiva y, por tanto, no es invertible. Lo más asombroso es que la IA utilizó 120 parámetros ajustables para controlar los 1329 coeficientes que teóricamente podían aparecer en el determinante jacobiano, logrando que todos los términos no nulos se cancelaran entre sí. En palabras de Tao: «Esto parece un milagro colosal.»
Lean + LLM: el matrimonio entre la creatividad y la prueba fehaciente
Una vez contada la historia, analicemos la lógica técnica.
Lean es un «compilador matemático». Cuando escribes una demostración matemática en Lean, cada inferencia debe pasar una verificación de tipos estricta. No existe eso de «los pasos obvios se omiten» — todo lo «obvio» debe desplegarse hasta el nivel atómico. Si el código compila, tu demostración es matemáticamente correcta, sin lugar a dudas, sin depender de la confianza de ningún juez humano.
El LLM (modelo de lenguaje grande) se encarga de la «ideación»; Lean se encarga del «veredicto». La debilidad inherente de los LLM al hacer matemáticas es que inventan — cuando no saben algo, escriben un razonamiento que parece plausible. La intervención de Lean resuelve este problema de raíz: el LLM genera código Lean, y el compilador lo verifica al instante. Si no compila, el LLM recibe el mensaje de error y puede corregirlo. La iteración continúa hasta que el código compila — y en ese punto, el resultado matemático generado por IA tiene una garantía de corrección rigurosa.
En marzo de 2026, un artículo titulado Learning to Disprove expuso sistemáticamente esta metodología. La idea central es: en lugar de pedirle al LLM que «demuestre» una proposición (propenso a inventar), es mejor pedirle que «encuentre contraejemplos» — porque una vez que el contraejemplo compila en Lean, la evidencia es irrefutable. Los autores adoptaron una estrategia de «mutación simbólica»: eliminar sistemáticamente ciertas condiciones de teoremas existentes para generar grandes cantidades de datos de entrenamiento donde se necesitan contraejemplos, y luego entrenaron al LLM con un sistema de recompensas múltiples. El resultado: la precisión del LLM en tareas de generación de contraejemplos mejoró un 49%.
Esta es la base técnica de la «superación por contraejemplos»: el LLM aporta la creatividad, Lean aporta la prueba fehaciente, y el matemático humano se convierte en espectador — al menos en lo que respecta a la verificación de resultados.
Las cinco fases del duelo en el mundo matemático
Buzzard documenta con franqueza las reacciones de los matemáticos que le rodean. En la hora del almuerzo en el Imperial College, escuchó a un colega decir: «Si los contraejemplos son tan fáciles de encontrar, es que los humanos no dedicamos suficiente tiempo a pensar en el problema.» Para sus adentros, esbozó una sonrisa amarga — él mismo había dedicado una semana entera a ese mismo problema «que no merecía la pena».
Esta es la fase típica de negación.
Después llegó la negociación. Un profesor envió un correo expresando su sorpresa: ¿por qué hay estudiantes de doctorado dispuestos a pagar 200 dólares al mes para suscribirse a Sol y Fable? La respuesta de Buzzard fue directa: «Cualquier estudiante de doctorado que no gaste esos 200 dólares está siendo irracional.» La Universidad de Harvard ya ha proporcionado acceso gratuito a Fable a todos sus estudiantes de doctorado, posdoctorados y profesores de matemáticas.
Independientemente de si emocionalmente se pueda aceptar, un hecho es claro: en la investigación matemática, la brecha de capacidad entre quienes dominan las herramientas de IA y quienes no, se está ensanchando por meses.
La dirección que marca Terence Tao
Entre todas las reacciones, la postura de Tao es quizás la más digna de atención. No cuestionó los límites de la IA ni cayó en el debate filosófico de «si esto sigue siendo matemáticas». Se sentó, escribió un artículo detallado, calculó la cuasihomogeneidad ponderada de los polinomios, ofreció una reconstrucción desde la perspectiva geométrica, e incluso publicó la transcripción completa de su conversación con GPT-5.
Es la actitud típica de un matemático de primera línea: el resultado está ahí; primero hay que entenderlo, luego usarlo.
En la discusión de HN, Tao señaló: «Esto nos dice que algunas construcciones matemáticas que parecían imposibles pueden encontrarse cuando el espacio de búsqueda es lo suficientemente grande.» La clave implícita de esta frase es que el espacio de búsqueda es inmenso, pero la IA nos ha enseñado cómo buscar. Y esto es solo el principio.
¿Qué le queda al matemático?
Si la IA puede encontrar contraejemplos, verificar demostraciones y formalizar teorías completas de forma autónoma, ¿qué le queda al matemático?
La respuesta de Buzzard es: comprender e interpretar. «El verdadero valor de estos ejemplos extraordinarios reside en la comprensión más profunda de las matemáticas que pueden aportar a los humanos», dice. Akhil Mathew ya está tratando de entender la estructura subyacente del contraejemplo de Grothendieck — preguntándose «qué está pasando realmente aquí», en lugar de conformarse con «es una construcción aleatoria y un cálculo coincidente».
La IA puede decirte «esto no se cumple», pero a menudo no puede decirte «qué significa esto para nuestro panorama matemático».
Históricamente, los matemáticos han externalizado una y otra vez el «cálculo» a las máquinas, para luego centrarse en niveles superiores de «comprensión» y «construcción». Ahora, «encontrar contraejemplos» y «verificar demostraciones» también se pueden externalizar. El trabajo humano que queda es quizás la parte más esencial de las matemáticas: cuando la máquina pone el contraejemplo sobre la mesa, comprender realmente por qué es importante — y qué podemos aprender de él.
Esto no es el fin de las matemáticas. Pero el papel del matemático está experimentando una evolución irreversible.
Referencias:
- Xenaproject — Artículo original de Kevin Buzzard «Human mathematicians are being outcounterexampled»
- Discusión en HN (id: 48998362) — Debate comunitario en torno al artículo de Tao sobre la conjetura Jacobiana
- Discusión en Lobsters (s/wfmpqr) — Comentarios en profundidad de la comunidad técnica sobre los contraejemplos matemáticos de la IA
- Blog de Terence Tao — Digestión y reconstrucción matemática del contraejemplo de la conjetura Jacobiana
- SBSeminar — Discusión de detalles matemáticos del nuevo contraejemplo de la conjetura Jacobiana
- arXiv 2603.19514 — Learning to Disprove: generación formal de contraejemplos con LLMs
- New Scientist — Reportaje sobre la resolución por IA de un problema matemático de 87 años
- GitHub DeepMind Formal Conjectures — Repositorio de conjeturas formalizadas, incluye el contraejemplo de la Jacobiana
