La irrupción de la inteligencia artificial en las matemáticas ha pasado en pocos años de la regurgitación de fórmulas básicas a la demostración autónoma de teoremas de nivel predoctoral. En el verano de 2025, sistemas de Google DeepMind y OpenAI alcanzaron la medalla de oro en la Olimpiada Internacional de Matemática, el equivalente al rendimiento de los estudiantes de secundaria más brillantes del mundo. Pocos meses después, la IA experimental Aletheia, de DeepMind, generó de forma autónoma resultados de investigación publicables a nivel de doctorado en geometría aritmética, y un modelo generalista de OpenAI refutó una conjetura relevante en geometría combinatoria, un hallazgo que matemáticos de primer nivel calificaron como un hito del razonamiento independiente de las máquinas.
Pero el avance no se limita a la capacidad de razonar. La combinación de grandes modelos de lenguaje con asistentes de demostración como Isabelle, Lean y Rocq, lenguajes de programación especializados que verifican la corrección lógica de cada paso, está automatizando la formalización de pruebas, una tarea que hasta ahora exigía a los humanos traducir manualmente sus teoremas a un formato legible por la máquina. La consecuencia es un cambio estructural: la máquina no solo acelera el cálculo, sino que empieza a asumir la conjectura, la estrategia de prueba y, en parte, la verificación.
Este escenario reabre preguntas de largo recorrido. Jeremy Avigad, matemático de la Universidad Carnegie Mellon, recuerda que lo que ha impulsado a los matemáticos durante siglos es una experiencia casi estética: la comprensión súbita tras horas de razonamiento. Krystal Maughan, doctoranda en la Universidad de Vermont, describe el silencio compartido en los seminarios de matemáticas puras como parte esencial del trabajo. Si la IA elimina ese proceso lento y deliberativo, ¿qué lugar queda para la intuición, la creatividad y la verificación humanas? Investigadores y filósofos debaten ahora si la disciplina debe redefinir su propósito: pasar de demostrar teoremas a enseñar a las máquinas a hacerlo, supervisar sus pruebas o, simplemente, seguir buscando la belleza de entender.