Hace cinco años, que un modelo de lenguaje resolviera matemáticas de varios pasos era casi una curiosidad. Hoy la pregunta ya no es solo si puede resolver ejercicios. Empieza a ser qué ocurre cuando también puede producir resultados de investigación.
El cambio importa por algo más profundo que una tabla de benchmarks. Durante siglos, obtener una demostración nueva ha sido una actividad escasa: podía requerir meses, décadas o una carrera completa. Alrededor de esa dificultad construimos publicaciones, reputación, formación y buena parte de la cultura matemática.
Si la producción de pruebas empieza a escalar computacionalmente, la escasez no desaparece. Se desplaza.
De los ejercicios a los problemas abiertos
La progresión reciente ayuda a entender por qué esta conversación ha cambiado tan rápido.
En 2021, OpenAI publicó GSM8K porque los modelos grandes seguían fallando de forma sistemática en problemas de primaria que exigían varios pasos. Un año después, Minerva, de Google, mejoró con claridad el rendimiento en problemas técnicos de instituto, universidad y ciencias cuantitativas.
En 2023, FunSearch combinó un modelo generador de programas con un evaluador automático. Encontró nuevas construcciones para el cap set problem y mejores heurísticas para bin packing. El salto conceptual era importante: el sistema no repetía una solución conocida, sino que buscaba candidatos que pudieran verificarse y conservarse si mejoraban el estado del arte.
En 2024, AlphaGeometry se acercó al nivel medio de un medallista de oro en un conjunto de problemas históricos de geometría olímpica. Ese mismo año, AlphaProof y AlphaGeometry 2 resolvieron cuatro de los seis problemas de la Olimpiada Matemática Internacional: 28 puntos sobre 42, nivel de plata.
En julio de 2025, una versión avanzada de Gemini Deep Think llegó al oro: cinco problemas resueltos, 35 puntos y demostraciones en lenguaje natural dentro del límite de 4,5 horas. La barrera simbólica de las competiciones había caído. Todavía quedaba una distinción cómoda: una olimpiada no es investigación.
En 2026 cambia la categoría de la evidencia
First Proof intentó medir precisamente esa frontera. Reunió diez problemas surgidos del trabajo real de matemáticos, con soluciones conocidas por sus autores pero aún no publicadas. Cuatro sistemas trabajaron bajo condiciones controladas y 30 especialistas revisaron las respuestas.
En siete de los diez problemas, al menos un sistema produjo una solución considerada esencialmente impecable o necesitada solo de correcciones menores. El propio informe contiene también la advertencia: los modelos tendían a detallar las partes rutinarias y a pasar demasiado rápido por los pasos difíciles; algunas citas no respaldaban lo afirmado.
Es un resultado mucho más útil que decir que «la IA ya hace matemáticas». Muestra capacidad real en una muestra pequeña, pero también los fallos que aparecen cuando una respuesta plausible debe superar una revisión de expertos.
Ese mismo año llegaron resultados más visibles. En mayo, OpenAI publicó un contraejemplo generado por un modelo interno que refutaba una conjetura de Erdős sobre distancias unitarias en el plano. Matemáticos externos revisaron la prueba y redactaron un artículo complementario para explicarla y situarla.
En agosto, OpenAI presentó diez resultados de su sistema interno Astra sobre problemas abiertos de geometría, teoría de códigos, grupos, complejidad, criptografía y combinatoria. La empresa afirma que el modelo generó los argumentos, que humanos los prepararon como manuscritos y que después el sistema formalizó cada uno en Lean. Son resultados públicos y comprobables, pero su recepción y relevancia a largo plazo todavía corresponden a la comunidad matemática, no al anuncio de una compañía.
Pocos días después, Anthropic comunicó otro avance llamativo. Una versión experimental de Claude intentó atacar la hipótesis de Riemann. No la resolvió. Durante el proceso produjo un argumento que eleva del 41,6% al 67,2% una cota inferior relacionada con la proporción de ceros de la función zeta que están sobre la línea crítica.
No significa que la hipótesis esté «resuelta al 67%». Anthropic dice explícitamente que no espera que esa técnica conduzca a una demostración. Dos matemáticos de la empresa validaron el trabajo, especialistas externos lo examinaron y existe una formalización en Lean. Es progreso en una cuestión relacionada, no una fracción de la conjetura principal.
Verificar una prueba no es comprenderla
Las matemáticas tienen una ventaja peculiar frente a otras ciencias. Una molécula propuesta por un modelo necesita un laboratorio. Una demostración puede traducirse a un objeto formal y ser comprobada paso a paso por un kernel pequeño. Lean no necesita confiar en la reputación de una empresa ni en la intuición del autor.
Pero la verificación formal responde a una pregunta limitada: ¿se sigue la conclusión de los axiomas y definiciones codificados mediante inferencias válidas? No responde si la prueba explica algo, si la formalización representa fielmente el enunciado que nos interesaba o si el resultado merece atención.
Una prueba de cien mil líneas puede ser correcta y seguir siendo inútil para una comunidad que no entiende su idea central. Tampoco basta con convertirla en prosa fluida. Una explicación demasiado pulida puede ocultar decisiones, intentos fallidos y conexiones que son precisamente lo que permite aprender del argumento.
De la escasez de pruebas a la indigestión
Terence Tao formula el problema como un posible paso de la escasez a la abundancia de demostraciones. Si asumimos que la IA podrá completar una fracción relevante de las tareas de investigación, aparece una cadena de cuellos de botella:
- generar una prueba candidata;
- verificar que es correcta;
- explicarla para que otros puedan entenderla;
- conseguir que la comunidad la evalúe y la use;
- integrarla en teorías, cursos y libros.
Automatizar el primer paso no automatiza los demás. Al contrario: puede inundarlos. Las pruebas pueden acumularse más rápido de lo que somos capaces de revisarlas, leerlas y convertirlas en conocimiento compartido.
El problema no empezó con la IA. La especialización, la longitud de algunos trabajos y la presión sobre la revisión académica ya habían creado una literatura difícil de digerir. La generación masiva puede multiplicar ese desajuste.
Lo valioso quizá nunca fue solo llegar al teorema
Resolver problemas es solo una parte de hacer matemáticas. También lo es elegir buenas preguntas, construir definiciones, descubrir conexiones, formar criterio, enseñar y mantener una comunidad capaz de transmitir conocimiento tácito.
Durante mucho tiempo esas actividades estaban correlacionadas. Para obtener una prueba difícil solía ser necesario comprender profundamente el problema; al hacerlo aparecían técnicas, intuiciones y nuevas preguntas. Por eso pudimos usar «demostrar un resultado» como indicador aproximado de todas las demás contribuciones.
La IA puede romper esa correlación. Si generar una prueba cuesta minutos pero comprender por qué funciona requiere meses, el resultado deja de ser una medida suficiente del trabajo valioso.
Eso obliga a plantear preguntas menos cómodas:
- ¿Quién recibe crédito por una prueba generada, seleccionada, verificada y explicada por actores distintos?
- ¿Cómo se forma un matemático si se automatizan justo los pasos difíciles mediante los que aprende?
- ¿Cómo se prioriza una literatura que crece más rápido que la capacidad humana de leerla?
- ¿Puede una teoría ser formalmente correcta sin que ninguna persona la comprenda en conjunto?
- ¿Qué debe conservarse como actividad humana incluso cuando pueda automatizarse?
La respuesta no será rechazar toda automatización ni aceptar cualquier resultado porque pase un verificador. Será diseñar procesos donde generación, validación, atribución y explicación estén separadas y sean visibles.
La IA no hace las matemáticas menos interesantes. Hace imposible seguir confundiendo producir pruebas con construir comprensión. Si demostrar deja de ser la parte difícil, quizá descubramos que lo valioso siempre estuvo también en saber qué demostrar, por qué importa y cómo hacerlo comprensible para los demás.
Fuentes
- OpenAI: Solving math word problems (GSM8K)
- Google Research: Minerva
- Google DeepMind: FunSearch
- Google DeepMind: AlphaProof y AlphaGeometry 2 en la IMO 2024
- Google DeepMind: Gemini Deep Think en la IMO 2025
- First Proof: informe de la segunda batería
- OpenAI: contraejemplo para la conjetura de distancias unitarias
- OpenAI: diez avances en matemáticas e informática teórica
- Anthropic: avance relacionado con la función zeta de Riemann
- Terence Tao: Mathematics in the age of AI
