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

Un grupo de investigadores publicó a principios de julio de 2026 en arXiv un artículo de posición que resume los logros de los demostradores de teoremas basados en LLM e identifica su límite fundamental: los sistemas actuales demuestran teoremas, pero no son capaces de descubrir matemáticas. Además, propone una hoja de ruta estratégica hacia agentes de investigación plenos.

Qué saben hacer hoy los sistemas AI4Math

En pocos años, los sistemas LLM para matemática formal han logrado un progreso notable. Con lenguajes de demostración interactiva de teoremas (ITP), sobre todo Lean 4, Isabelle y Coq, han aprendido a generar demostraciones formales para problemas bien planteados. Estos lenguajes permiten escribir las demostraciones de modo que un ordenador pueda verificar mecánicamente cada paso, lo que hace el resultado mucho más fiable que las demostraciones manuscritas tradicionales.

Los autores agrupan el avance del campo en tres líneas clave:

• Conjuntos de datos: se han acumulado corpus de problemas formalizados, desde nivel escolar hasta universitario, que permiten entrenar modelos con ejemplos de demostraciones correctas
• Autoformalización: los modelos han mejorado al traducir enunciados escritos en lenguaje natural a la sintaxis formal estricta de los ITP
• Síntesis de demostraciones: los sistemas encuentran con cada vez más soltura demostraciones paso a paso cuando se les da un planteamiento inicial claro

Todos estos avances tienen algo en común: solo funcionan con problemas bien definidos y formulados de antemano. El modelo sabe qué tiene que demostrar y busca el camino hacia esa meta.

Por qué esto todavía no es ciencia

La verdadera ciencia matemática se distingue de manera fundamental de resolver un libro de ejercicios. Exige saber formular conjeturas, detectar conexiones inesperadas entre áreas distintas y atacar problemas abiertos, a menudo de muchos años, mal delimitados y que implican varios niveles de abstracción. Es aquí donde los sistemas LLM actuales muestran limitaciones sistemáticas.

Los autores destacan cinco problemas clave:

• Datos: los conjuntos de datos no contienen ejemplos de cómo nacen los nuevos teoremas, solo la resolución de problemas ya planteados
• Estructura: la matemática se apoya en jerarquías complejas de conceptos y en dependencias implícitas entre ramas, que los LLM asimilan mal
• Investigación: los modelos saben responder preguntas, pero no formular otras nuevas, que es la base de la ciencia
• Herramientas: no hay integración con sistemas de álgebra computacional ni con bases de datos matemáticas especializadas
• Colaboración: los modelos no pueden ser coautores de pleno derecho, porque no entienden el contexto informal que los científicos se transmiten entre sí

«El próximo gran avance en AI4Math exige un cambio decisivo: pasar de

resolutores de problemas predefinidos a agentes de investigación capaces de trabajar en la frontera de las matemáticas», tesis central del artículo.

Cómo debería ser el próximo sistema

La hoja de ruta estratégica del artículo plantea avanzar hacia agentes matemáticos de investigación: sistemas capaces de formular conjeturas por sí mismos, planificar un programa de investigación, interactuar con los científicos en forma de diálogo y refinar de manera iterativa el planteamiento del problema.

Para ello habrá que desarrollar a la vez varias áreas: nuevos conjuntos de datos con ejemplos de descubrimientos reales, métodos para trabajar con las estructuras relacionales de las matemáticas, ecosistemas de herramientas más maduros y modelos de colaboración entre personas y máquinas radicalmente distintos. Ninguno de estos componentes existe todavía en la forma necesaria, lo que hace que la tarea sea enorme, pero esté claramente formulada.

Qué significa esto

El artículo señala un cambio importante en el horizonte de tareas de AI4Math: de sistemas que verifican demostraciones a sistemas capaces de participar en el descubrimiento de nuevas matemáticas. Esta transición exige una arquitectura radicalmente distinta de la simple ampliación de escala de los enfoques actuales. Si se cumple la hoja de ruta propuesta, las matemáticas podrían convertirse en una de las primeras áreas en que la IA actúe como un verdadero socio de investigación del científico.