IA en matemáticas: sistemas de inteligencia artificial que demuestran teoremas, resuelven problemas olímpicos y de investigación, y verifican demostraciones. El papel clave lo tiene el lenguaje formal Lean: una demostración escrita en él la verifica un ordenador, así que el resultado de la IA se puede comprobar sin fiarse del propio modelo.
En tres años, el campo pasó del nivel de medalla de plata olímpica (2024) a cientos de manuscritos con resultados nuevos (2026).12 Eso ha provocado entre los matemáticos tanto entusiasmo como inquietud: Terence Tao habla de la llegada de una «era de abundancia de demostraciones», y la Unión Matemática Internacional respaldó una declaración según la cual las matemáticas deben seguir siendo cosa de personas.34
Historia
- 14.12.2023Google DeepMind publica en Nature el sistema FunSearch: un modelo de lenguaje, junto con una verificación automática, encontró nuevas construcciones de cap sets grandes, mejores que las conocidas hasta entonces.5 ¶ cza2rk877
- 25.07.2024Los sistemas de DeepMind AlphaProof y AlphaGeometry 2 resuelven cuatro de los seis problemas de la Olimpiada Internacional de Matemáticas: 28 puntos, nivel de medalla de plata; un problema en minutos, los demás en hasta tres días. AlphaProof combina un modelo de lenguaje preentrenado con el algoritmo de aprendizaje por refuerzo AlphaZero y demuestra afirmaciones en Lean.1 ¶ cpmp95wjd
- 14.05.2025AlphaEvolve de DeepMind encuentra una forma de multiplicar matrices complejas de 4×4 con 48 multiplicaciones escalares, mejor que el algoritmo de Strassen de 1969. En algo más de 50 problemas abiertos, el sistema igualó las mejores soluciones conocidas en cerca del 75% de los casos y las mejoró en el 20%.6 ¶ cz2yux3ij
- 19.07.2025OpenAI afirma que su modelo de razonamiento experimental obtuvo en la olimpiada un resultado de nivel de medalla de oro.7 ¶ ccp7fkcq7
- 21.07.2025Gemini Deep Think de DeepMind obtiene oficialmente el oro en la olimpiada: cinco de seis problemas resueltos por completo, 35 de 42 puntos, dentro de las 4,5 horas de la competición; el resultado lo evaluaron y confirmaron oficialmente los coordinadores de la olimpiada con los mismos criterios que las soluciones de los estudiantes.8 ¶ c4xkfkcjr
- 08.09.2026OpenAI informa de que su modelo interno demostró la posibilidad de una singularidad en las ecuaciones de Navier-Stokes (con fuerza externa), usando unos 10 000 agentes durante 88 horas; la demostración está formalizada en Lean.9 ¶ cfknhmsr6
- 08.10.2026Science publica el artículo de DeepMind sobre el agente AlphaProof Nexus: resolvió por su cuenta 9 de 353 problemas abiertos de Erdős y demostró 44 de 492 conjeturas de la Enciclopedia en línea de secuencias de enteros (OEIS), con todas las demostraciones verificadas en Lean. En el mismo número los matemáticos Jeremy Avigad y Matthew Ballard firman la columna «Ha llegado la IA para la investigación matemática».10 ¶ ckdzaxmkz
Cómo funciona
Hay dos enfoques. En el primero, el modelo busca soluciones en forma de programas o construcciones, y un evaluador automático comprueba si son mejores que las conocidas: así funcionan FunSearch y AlphaEvolve. En el segundo, el modelo escribe la demostración en el lenguaje formal Lean y la verifica un ordenador: así funcionan AlphaProof y el proyecto Gauss de la empresa Math Inc, que en tres semanas formalizó la forma fuerte del teorema sobre la distribución de los números primos (unas 25 000 líneas de Lean), un reto planteado por Tao y Alex Kontorovich en enero de 2024.11 ¶ c6575vwd8
Datos
| estudio | qué se midió | resultado |
|---|---|---|
| Epoch AI, FrontierMath, 07.11.202412 | problemas nuevos y difíciles de nivel de matemáticas de investigación | los mejores modelos resolvían menos del 2% de los problemas ¶ cc9ttcnpr |
| OpenAI, 06.10.20262 | resultados del modelo interno publicados en GitHub; estimación de la propia empresa | 719 manuscritos en 372 grupos, unos 4000 problemas planteados; un resultado equivale de media a unas tres horas de trabajo de ChatGPT Pro en modo de razonamiento; tres manuscritos se retiraron poco después por un error de signo ¶ cghjnybxm |
En dos años, la IA pasó de «menos del 2%» en problemas de investigación y de la plata olímpica a cientos de manuscritos con resultados nuevos. La verificabilidad es la principal diferencia entre las matemáticas y otros campos: una demostración en Lean la verifica un ordenador, así que aquí la velocidad de la IA no choca con la confianza en el modelo, sino con la capacidad de las personas para entender e integrar los resultados. Salvedades: parte de las afirmaciones son estimaciones internas de las empresas, y los resultados más sonados de OpenAI los produjo un modelo que no se puede verificar desde fuera. ¶ c8xxc87et
Críticas
En octubre de 2025, unos investigadores anunciaron que, con ayuda de GPT-5, habían encontrado soluciones a 10 problemas de Erdős que figuraban como abiertos. El responsable de la base de datos erdosproblems.com, Thomas Bloom, calificó la presentación de «una tergiversación dramática»: GPT-5 había encontrado artículos ya publicados con las soluciones que él personalmente no conocía, y el estado «abierto» solo significaba que él no conocía ningún artículo así. Según él, la capacidad del modelo para buscar bibliografía «ya es lo bastante útil e impresionante, ¡no hace falta describirla como algo que no es!».13 ¶ cydu4nn57
Tras la publicación de OpenAI, The Verge habló con más de treinta matemáticos; Bartosz Naskręcki dijo que esto «puede provocar un enorme colapso de la cultura académica».14 ¶ c6fm7zxay
Scientific American contó el 13.10.2026 que los matemáticos, tras analizar la demostración de 166 páginas de OpenAI sobre las ecuaciones de Navier-Stokes, vieron que construye la fuerza externa de un modo totalmente distinto al del programa de los españoles Diego Córdoba y Luis Martínez-Zoroa, aunque al publicarla la propia empresa afirmó «clara y repetidamente» que seguía ese programa.15 ¶ cdpxcquac
Timothy Gowers definió su mayor temor respecto a la IA en matemáticas como «la posible destrucción de la cultura matemática»: el conocimiento y la experiencia que no solo existen en la bibliografía, sino también en la cabeza de los matemáticos.16 ¶ czth2y863
Evolución
El 02.06.2026 se publicó la Declaración de Leiden sobre la IA y las matemáticas, respaldada por la Unión Matemática Internacional: el mérito y la responsabilidad siguen correspondiendo a las personas dentro de la comunidad matemática y no deben atribuirse a sistemas automatizados.4 ¶ cxrzjmjxp
Tao propone dejar de perseguir a ciegas la resolución de problemas: en la era de abundancia de demostraciones, según él, eso ya perjudica la salud a largo plazo de las matemáticas.3
Señales
- Ciencia / Jack Clark: «La IA se vuelve creativa, tanto en matemáticas como en la investigación sobre la propia IA, así que la automejora recursiva completa ahora es más probable que sea posible en 2027 que en 2028»cofundador de Anthropic, en su boletín Import AI, a propósito de una prueba del olfato investigador de los modelos; en mayo cifró en un 60% la probabilidad de que a finales de 2028 un modelo pueda entrenar por sí solo a su sucesor
- Ciencia / Terence Tao: «Estamos entrando en una era de abundancia de demostraciones»en su conferencia «Math 2.0» en Caltech, sobre lo que la IA ha hecho con las matemáticas
- Ciencia / Hugo Duminil-Copin: «La publicación por OpenAI de cientos de demostraciones de IA es un «choque monumental»: para los matemáticos «es el día después»; en uno de los problemas sintió que corría un maratón con alguien a cuestas que se bajó en los últimos 100 metros para cruzar la meta antes que él»matemático francés, medalla Fields 2022, en la radio suiza RTS después de que OpenAI publicara cientos de manuscritos con demostraciones de IA, 16 de ellos sobre problemas de su campo
- Ciencia / Timothy Gowers: «Demostrar algo que los LLM no puedan demostrar»un medallista Fields, sobre ChatGPT produciendo en una hora una investigación de nivel doctoral
Véase también
Referencias
-
AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind, 25.07.2024. deepmind.google ↩ ↩2
-
openai/math — OpenAI, GitHub, 06.10.2026. github.com ↩ ↩2
-
Math 2.0 — Terence Tao, 10.10.2026. terrytao.wordpress.com ↩ ↩2
-
Leiden Declaration on Artificial Intelligence and Mathematics — 02.06.2026. leidendeclaration.ai ↩ ↩2
-
B. Romera-Paredes et al. Mathematical discoveries from program search with large language models — Nature, 14.12.2023. nature.com ↩
-
AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms — Google DeepMind, 14.05.2025. deepmind.google ↩
-
Alexander Wei: «our latest @OpenAI experimental reasoning LLM has achieved … gold medal-level performance» — X, 19.07.2025. x.com ↩
-
Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad — Google DeepMind, 21.07.2025. deepmind.google ↩
-
On the Navier–Stokes Millennium Prize Problem — OpenAI, 08.09.2026. openai.com ↩
-
Tsoukalas et al. Advancing mathematics research with AI-driven formal proof search — Science, 08.10.2026. doi.org ↩
-
Introducing Gauss, an agent for autoformalization — Math, Inc. math.inc ↩
-
E. Glazer et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI — arXiv, 07.11.2024. arxiv.org ↩
-
Thomas Bloom: «this is a dramatic misrepresentation» — X, 17.10.2025. x.com ↩
-
‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop — The Verge, 09.10.2026. theverge.com ↩
-
OpenAI’s blockbuster Navier-Stokes proof isn’t what we thought it was — Scientific American, 13.10.2026. scientificamerican.com ↩
-
Thoughts about the Leiden Declaration — Timothy Gowers, 26.07.2026. gowers.wordpress.com ↩