Los modelos de IA están empezando a resolver problemas matemáticos sofisticados

Durante el fin de semana, Neel Somani, ingeniero de software, ex investigador cuántico y fundador de una startup, estaba probando las capacidades matemáticas del nuevo modelo de OpenAI cuando hizo un descubrimiento inesperado. Después de poner el problema en ChatGPT y dejarlo pensar durante 15 minutos, regresó con una solución completa. Evaluó la prueba y la formalizó con una herramienta llamada Harmonic, pero todo funcionó.

“Quería establecer una línea de base para saber cuándo los graduados de LLM son realmente capaces de resolver problemas matemáticos abiertos en comparación con aquellos con los que tienen dificultades”, dijo Somani. La sorpresa fue que el límite avanzó un poco con el último modelo.

Aún más impresionante es la cadena de pensamiento de ChatGPT, que recita axiomas matemáticos como la fórmula de Legendre, el postulado de Bertrand y el teorum de la estrella de David. Finalmente, el modelo encontró una publicación de Math Overflow de 2013 en la que el matemático de Harvard Noam Elkies proporcionó una solución elegante a un problema similar. Sin embargo, la prueba final de ChatGPT difería del trabajo de Elkies en aspectos importantes, proporcionando una solución más completa a una versión del problema del legendario matemático Paul Erdős, cuya extensa colección de problemas sin resolver se ha convertido en un campo de pruebas para la IA.

Para cualquiera que sea escéptico respecto de la inteligencia artificial, este es un resultado sorprendente, y no es el único. Las herramientas de IA se han vuelto omnipresentes en matemáticas, desde LLM centrados en la formalización como Harmonics Aristotle hasta herramientas de investigación literaria como Deep Research de OpenAI. Pero desde el lanzamiento de GPT 5.2, que Somani describe como “anecdóticamente más hábil en el razonamiento matemático que las iteraciones anteriores”, el gran volumen de problemas resueltos se ha vuelto difícil de ignorar y plantea nuevas preguntas sobre la capacidad de los grandes modelos de lenguaje para ampliar los límites del conocimiento humano.

Somani abordó los Problemas de Erdős, una serie de más de mil conjeturas del matemático húngaro que se mantienen en línea. Los problemas se han convertido en un objetivo tentador para las matemáticas impulsadas por la IA y varían significativamente tanto en el tema como en el nivel de dificultad. Las primeras soluciones autónomas surgieron en noviembre de un modelo basado en Gemini llamado AlphaEvolve, pero más recientemente Somani y otros descubrieron que GPT 5.2 puede manejar matemáticas sofisticadas notablemente bien.

Desde Navidad, 15 problemas en el sitio web de Erdős han pasado de “abiertos” a “resueltos”, y 11 de las soluciones indican específicamente que los modelos de IA están involucrados en el proceso.

El venerado matemático Terence Tao ofrece una mirada más matizada al progreso en su página de GitHub, enumerando ocho problemas diferentes en los que los modelos de IA lograron avances autónomos significativos en un problema de Erdős, así como otros seis casos en los que se lograron avances al encontrar y aprovechar investigaciones previas. Todavía queda un largo camino por recorrer antes de que los sistemas de IA sean capaces de realizar cálculos sin intervención humana, pero está claro que los modelos grandes tienen un papel importante que desempeñar.

Con respecto a Mastodon, Tao conjeturó que la escalabilidad de los sistemas de IA los hace “más adecuados para ser aplicados sistemáticamente a la 'larga cola' de oscuros problemas de Erdős, muchos de los cuales en realidad tienen soluciones simples”.

“Como resultado, muchos de estos problemas más simples de Erdős ahora se resuelven más fácilmente utilizando métodos puramente basados ​​en IA que con medios humanos o híbridos”, continuó Tao.

Otra fuerza impulsora es el reciente cambio hacia la formalización, una tarea que requiere mucha mano de obra y que facilita probar y ampliar el pensamiento matemático. La formalización no requiere el uso de IA ni computadoras, pero una nueva generación de herramientas automatizadas ha simplificado enormemente el proceso. El “asistente de pruebas” de código abierto Lean, desarrollado en Microsoft Research en 2013, se utiliza ampliamente en el campo como método para formalizar pruebas, y herramientas de inteligencia artificial como Harmonics Aristotle prometen automatizar gran parte del trabajo de formalización.

Para el fundador de Harmonic, Tudor Achim, el salto repentino hacia los problemas resueltos de Erdő es menos importante que el hecho de que los matemáticos más importantes del mundo están empezando a tomar en serio estas herramientas. “El hecho de que los profesores de matemáticas e informática utilicen (herramientas de inteligencia artificial) es más importante para mí”, dijo Achim. “Estas personas tienen que proteger su reputación, por lo que cuando dicen que usan Aristóteles o ChatGPT, eso es evidencia real”.