Los LLM demuestran teoremas, pero no descubren matemáticas: investigadores describen el siguiente paso

Un grupo de investigadores publicó un artículo de posicionamiento en arXiv a principios de julio de 2026 que sistematizó los logros de los proveedores de teoremas basados en LLM e identificó su limitación fundamental: los sistemas actuales demuestran teoremas pero son incapaces de descubrir matemáticas — y propuso una hoja de ruta estratégica para la transición a agentes de investigación completamente desarrollados.

Lo Que los Sistemas AI4Math Pueden Hacer Hoy

En los últimos años, los sistemas LLM para matemáticas formales han logrado un progreso tangible. Trabajando con lenguajes para prueba interactiva de teoremas (ITP) — principalmente Lean 4, Isabelle y Coq — han aprendido a generar pruebas formales para problemas bien definidos. Estos lenguajes permiten que las pruebas se escriban de manera que una computadora pueda verificar mecánicamente cada paso — haciendo que el resultado sea fundamentalmente más confiable que las pruebas manuscritas tradicionales.

Los autores sistematizaron tres direcciones clave de desarrollo del campo:

• Conjuntos de datos — se han acumulado corpus de problemas formalizados, desde el nivel de escuela secundaria hasta universitario, que permiten entrenar modelos con ejemplos de pruebas correctas
• Autoformalización — los modelos han mejorado en la traducción de enunciados de problemas escritos en lenguaje natural a la sintaxis formal rigurosa de ITP
• Síntesis de pruebas — los sistemas están cada vez más seguros de encontrar pruebas paso a paso cuando se les proporciona una formulación inicial clara

Todos estos logros comparten una característica: funcionan solo en problemas bien definidos y pre-formulados. El modelo sabe exactamente qué se debe demostrar — y busca el camino hacia ese objetivo.

Por Qué Esto Aún No Es Ciencia

La verdadera ciencia matemática es fundamentalmente diferente de resolver problemas de un libro de ejercicios. Requiere la capacidad de formular hipótesis, identificar conexiones inesperadas entre diferentes dominios y atacar problemas abiertos — a menudo de larga data, mal formulados y que requieren múltiples niveles de abstracción. Es precisamente aquí donde los sistemas LLM actuales demuestran limitaciones sistémicas.

Los autores identifican cinco problemas clave:

• Datos: los conjuntos de datos no contienen ejemplos de cómo nacen los nuevos teoremas — solo soluciones de problemas ya planteados
• Estructura: la matemática se basa en jerarquías complejas de conceptos y dependencias implícitas entre ramas, que los LLM asimilan mal
• Exploración: los modelos pueden responder preguntas pero no formular nuevas — y esto es lo fundamental de la ciencia
• Herramientas: no hay integración con sistemas de álgebra computacional y bases de datos matemáticas especializadas
• Colaboración: los modelos no pueden ser colaboradores completos — no entienden el contexto informal que los científicos se transmiten entre sí

"El siguiente avance en AI4Math requiere un cambio decisivo de

solucionadores de tareas predeterminadas a agentes de investigación capaces de trabajar en la frontera de las matemáticas" — la tesis clave del artículo.

Cómo Debería Ser el Siguiente Sistema

La hoja de ruta estratégica descrita en el artículo prevé una transición a agentes de investigación matemática — sistemas capaces de formular independientemente hipótesis, planificar programas de investigación, interactuar con científicos en modo de diálogo y refinar iterativamente las formulaciones de problemas.

Esto requerirá el desarrollo simultáneo de varias direcciones: nuevos conjuntos de datos con ejemplos de descubrimientos reales, métodos para trabajar con estructuras relacionales de las matemáticas, ecosistemas de herramientas más maduros y modelos fundamentalmente diferentes de colaboración humano-máquina. Ninguno de estos componentes existe aún en la forma necesaria — lo que hace que la tarea sea a gran escala pero claramente formulada.

Qué Significa Esto

El artículo señala un cambio importante en el horizonte de AI4Math: de sistemas para verificación de pruebas a sistemas capaces de participar en el descubrimiento de nuevas matemáticas. Esta transición requiere una arquitectura fundamentalmente diferente de simplemente escalar los enfoques existentes. Si la hoja de ruta propuesta se realiza, las matemáticas podrían convertirse en uno de los primeros campos donde la IA se convierte en un verdadero socio de investigación del científico.