La Inteligencia Artificial Empieza a Resolver Problemas Complejos de Matemáticas

Quince problemas de Paul Erdős han pasado de “abiertos” a “resueltos” desde Navidad, y en once de esos casos se acredita explícitamente la participación de modelos de IA. La matemática de alto nivel empieza a notar, cada vez con menos disimulo, el zumbido de los LLM justo detrás.

El caso que encendió la mecha lo cuenta Neel Somani, ingeniero de software, exinvestigador cuantitativo y fundador de una start-up. Durante un fin de semana decidió poner a prueba al nuevo modelo de OpenAI, GPT 5.2, así que Somani pegó el enunciado en ChatGPT y le dejó “pensar” durante unos quince minutos. Cuando volvió, el modelo había producido una solución completa.

Por supuesto, una “solución” en un chat no vale nada si no se puede verificar. Así que Somani hizo lo que haría cualquiera que no quiera vender humo: revisó la demostración y la formalizó con Harmonic, superando la verificación.

La historia no es “la IA es lista”, sino “la IA empieza a cerrar pruebas”

Somani no estaba persiguiendo un truco viral. Su objetivo era mucho más sobrio: establecer una línea base sobre cuándo los LLM pueden resolver problemas matemáticos abiertos y en qué punto empiezan a atascarse. Según explica, con el modelo más reciente “la frontera” de lo resoluble por un LLM se ha desplazado. No significa que ahora todo sea sencillo, pero sí que el borde del mapa se ha movido.

Lo llamativo es el tipo de razonamiento que describe. La cadena de pensamiento destacaba por enumerar axiomas y resultados avanzados, desde la fórmula de Legendre hasta el postulado de Bertrand o el teorema de la Estrella de David. No es un “probé dos casos y funcionó”, sino un hilo argumental que suena a matemático humano usando su caja de herramientas habitual.

A esto se suma un detalle muy propio de 2026: el modelo localizó una publicación de Math Overflow de 2013 en la que el matemático de Harvard Noam Elkies proponía una solución elegante a un problema similar. Es decir, además de razonar, hizo una revisión bibliográfica útil, algo que en investigación suele equivaler a media victoria.

Lo más interesante es que la prueba final de ChatGPT no era un simple calco de Elkies. Difería en aspectos clave y aportaba una solución más completa para una versión del problema atribuida a Paul Erdős.

Los “Erdős problems” se están convirtiendo en el benchmark incómodo

La colección de problemas no resueltos de Erdős —más de mil conjeturas mantenidas online— se ha convertido en un objetivo especialmente tentador para la matemática asistida por IA.

El atractivo está en su variedad extrema: los problemas cambian radicalmente de temática y dificultad, lo que los convierte en un banco de pruebas de “larga cola” más que en un escaparate de unos pocos desafíos famosos.

Esto no debe leerse como “la IA ya hace matemáticas sola”. La interpretación general es bastante más prudente: todavía estamos lejos de sistemas que investiguen sin intervención humana, pero los modelos grandes ya ocupan un hueco real en el proceso.

Incluso dentro del entusiasmo hay matices. El matemático Terence Tao ofrece una lectura más fina y contabiliza ocho problemas distintos en los que la IA logró progreso autónomo significativo sobre un problema de Erdős. Además, recoge seis casos en los que el avance vino de localizar y construir sobre investigación previa. A veces la IA “descubre”, y otras hace algo que muchos humanos no hacen bien: encontrar lo relevante y conectar piezas con rapidez.

Formalización: la parte aburrida que lo cambia todo

Hay otra fuerza empujando este cambio, menos vistosa que el titular de “IA resuelve conjetura”, pero posiblemente más transformadora: la formalización.

Formalizar una demostración significa convertirla en algo que una herramienta pueda verificar paso a paso. Obliga a eliminar huecos, a reducir los “esto es evidente” y a dejar menos espacio para la intuición implícita.

La formalización no requiere necesariamente IA ni siquiera ordenadores, pero las herramientas actuales hacen el proceso mucho más llevadero. El asistente de pruebas Lean, desarrollado en Microsoft Research en 2013, se ha consolidado como una vía habitual para formalizar demostraciones, mientras que herramientas como Aristotle, de Harmonic, prometen automatizar gran parte del trabajo pesado.

Para Tudor Achim, fundador de Harmonic, lo realmente relevante no es un sprint de quince problemas resueltos, sino que matemáticos de primer nivel estén empezando a tomarse estas herramientas en serio. Cuando profesores de matemáticas e informática, con reputaciones que proteger, reconocen que usan estas IAs, no es postureo. Es una señal clara de utilidad real dentro del flujo de trabajo.

Si GPT 5.2 es “anecdóticamente” mejor en razonamiento matemático, como dice Somani, la pregunta ya no es si estas máquinas pueden ayudar. La pregunta es cuántos problemas “medianos” siguen ahí fuera, esperando a que alguien —humano o IA— los encuentre y se ponga a trabajar en ellos.