Durante años, la frontera parecía clara. Los modelos de inteligencia artificial podían ayudar a calcular, comprobar casos o resumir artículos, pero los problemas matemáticos abiertos de alto nivel seguían siendo territorio humano. Ese límite empieza a moverse. Y lo hace de forma incómoda para muchas certezas académicas.
El detonante más reciente llegó el pasado fin de semana. Neel Somani, ingeniero de software y fundador de varias startups, decidió someter al nuevo modelo de OpenAI a una prueba poco habitual: resolver un problema matemático complejo que no tenía una solución cerrada conocida. Introdujo el enunciado en ChatGPT, dejó al sistema razonar durante unos 15 minutos y esperó.
La respuesta no fue un boceto ni una intuición. El modelo devolvió una solución completa, con razonamiento estructurado y referencias a resultados clásicos. Somani revisó paso a paso el proceso y formalizó la demostración con Harmonic, una herramienta de verificación matemática. El resultado cuadraba. No había trampas evidentes.
Una frontera que se desplaza
Somani quería medir hasta dónde llegan hoy los grandes modelos de lenguaje en matemáticas puras y, sobre todo, dónde siguen fallando. La sorpresa fue constatar que el límite no es el mismo que hace un año. La frontera de lo resoluble se ha desplazado, aunque sea unos metros.
El resultado se apoyó en axiomas y resultados conocidos, como la fórmula de Legendre o el postulado de Bertrand, y fue capaz de encajar esas piezas en un argumento coherente. En un momento dado, incluso identificó un hilo de Math Overflow de 2013 en el que Noam Elkies, matemático de Harvard, había resuelto un problema relacionado.
Aquí está uno de los puntos clave. La demostración generada por la IA no era una copia. Difería en aspectos relevantes y ofrecía una solución más completa a una variante planteada por Paul Erdős, una figura legendaria cuya lista de conjeturas abiertas sigue siendo un campo de pruebas para generaciones de matemáticos.
No es un caso aislado
Este episodio no ocurre en el vacío. Desde el lanzamiento de GPT-5.2, que Somani considera claramente más competente en razonamiento matemático que versiones anteriores, el número de problemas resueltos con ayuda de IA ha aumentado de forma visible.
Hay un dato difícil de ignorar. En el sitio web que recopila los problemas de Erdős, desde Navidad se han reclasificado 15 conjeturas de “abiertas” a “resueltas”. En 11 de esos casos, se reconoce de forma explícita la participación de modelos de inteligencia artificial en el proceso. Hablamos de problemas que llevaban años, a veces décadas, esperando una solución formal aceptable.
La mirada prudente de los matemáticos
No todos están eufóricos. Terence Tao, uno de los matemáticos más influyentes del mundo, ofrece una lectura más matizada. En su repositorio público distingue entre distintos niveles de aportación de la IA.
En algunos problemas, los modelos han logrado avances autónomos reales. En otros, su contribución ha consistido en localizar trabajos previos, combinarlos y extenderlos de forma eficiente. Eso no sustituye al matemático, pero cambia su papel.
Tao apunta además a un factor estructural. La IA es especialmente buena atacando aquellos problemas menos conocidos y menos glamurizados, donde la solución puede ser directa pero nadie ha tenido tiempo o incentivos para formalizarla.
La clave está en la formalización
Detrás de este salto hay algo menos visible que los modelos de lenguaje. La formalización matemática se ha convertido en el gran acelerador. Formalizar significa expresar una demostración de forma que pueda ser verificada, reutilizada y ampliada sin ambigüedades.
Herramientas como Lean, desarrollado en Microsoft Research, o Harmonic, permiten reducir drásticamente la carga manual. Un ejemplo concreto: una demostración que antes exigía semanas de revisión humana puede ahora validarse en horas si está correctamente formalizada.
Para Tudor Achim, fundador de Harmonic, el dato más relevante no es cuántos problemas se resuelven, sino quién está usando estas herramientas. Cada vez más profesores e investigadores consolidados reconocen abiertamente su apoyo en sistemas de IA para explorar y verificar resultados.
Ese reconocimiento público marca un cambio cultural. La IA deja de ser un truco experimental y empieza a ocupar un lugar legítimo en la investigación matemática avanzada.
Por ahora, los modelos no generan nuevas teorías profundas de forma autónoma. Pero sí hacen algo muy valioso: exploran, combinan y formalizan a una escala que ningún humano puede igualar. En campos donde la verificación sistemática es clave, eso cambia las reglas.
Lo que estamos viendo no es el final de la matemática humana. Es el inicio de una colaboración desigual. La IA no piensa como un matemático, pero empieza a trabajar como uno. Y en algunos problemas, eso ya está siendo suficiente para mover fronteras que parecían inamovibles.
