El 12 de septiembre de 2026, Steven Strogatz describió una tensión que va mucho más allá de una nueva demostración: la IA está acelerando la investigación matemática, pero también amenaza con desplazar parte de la comprensión, el reconocimiento y la motivación que daban sentido a la profesión. En paralelo, OpenAI había afirmado el 8 de septiembre que sus sistemas habían producido un resultado sobre Navier–Stokes, mientras Anthropic comunicó el 4 de septiembre que Claude había formalizado una demostración existente de Fermat. Son logros distintos y ninguno permite saltarse la evaluación matemática humana.
Dos avances de IA que no significan lo mismo
La afirmación de OpenAI apunta a una posible construcción nueva para un caso concreto de las ecuaciones de Navier–Stokes. El proyecto de Anthropic, en cambio, convirtió en una formalización verificable una demostración que ya existía: el trabajo asociado a Andrew Wiles y Richard Taylor sobre el último teorema de Fermat.
| Sujeto | Objetivo matemático | Situación actual | Qué deben evaluar los expertos | Papel humano en discusión |
| OpenAI | Construcción que, según la empresa, produce una singularidad en tiempo finito en ecuaciones forzadas, tridimensionales e incompresibles de Navier–Stokes | Afirmación de la empresa sin aceptación matemática independiente | Si resuelve exactamente la cuestión planteada y si el argumento resiste el escrutinio especializado | Comprender el argumento, comprobar su alcance y valorar su relevancia |
| Anthropic y Claude | Formalización en Lean de una demostración existente del último teorema de Fermat | Formalización comunicada por Anthropic, no descubrimiento de un teorema nuevo | Si el desarrollo formal refleja fielmente la demostración y sus supuestos | Traducir, interpretar y contextualizar una prueba extensa |
La distinción parece académica, pero cambia por completo el titular correcto. Formalizar una prueba conocida puede ser una hazaña de ingeniería matemática; no equivale a descubrir el resultado. Y una construcción acompañada de código que se ejecuta no se convierte automáticamente en una solución aceptada.
Qué afirmó exactamente OpenAI sobre Navier–Stokes
OpenAI comunicó el 8 de septiembre de 2026 que sus sistemas habían producido una prueba analítica y una formalización en Lean relacionada con una singularidad en tiempo finito. El caso descrito corresponde a ecuaciones de Navier–Stokes forzadas, tridimensionales e incompresibles, con las condiciones matemáticas indicadas por la empresa.
Una singularidad de este tipo significa que una magnitud del modelo, como la velocidad, crecería sin límite en un tiempo finito. No describe literalmente que el agua o el aire reales alcancen una velocidad infinita: es una afirmación sobre el comportamiento límite de unas ecuaciones continuas.
El problema de existencia y regularidad de Navier–Stokes forma parte de los siete Problemas del Milenio del Clay Mathematics Institute, asociados a un premio de un millón de dólares cada uno. La afirmación de OpenAI sigue necesitando evaluación matemática independiente para determinar qué problema resuelve exactamente y si su construcción es válida en el sentido aceptado por la comunidad.
El detalle técnico importa porque no todas las ecuaciones de fluidos plantean la misma pregunta. Navier–Stokes forzado, las ecuaciones de Euler y las ecuaciones de Boussinesq no son intercambiables; cambiar la fuerza externa, la dimensión o las condiciones altera el problema.
Qué hizo Claude con la demostración de Fermat
Anthropic comunicó el 4 de septiembre de 2026 que agentes de Claude formalizaron en Lean una demostración existente del último teorema de Fermat. El proyecto probó unos 29.500 teoremas intermedios utilizados en la demostración final, dentro de un desarrollo mucho más amplio.
Eso no significa que Claude descubriera el teorema. La aportación descrita consiste en expresar una prueba matemática ya establecida dentro de un sistema formal que puede comprobar sus pasos. El reto cambia: en lugar de encontrar el resultado desde cero, hay que traducir una arquitectura matemática compleja a un lenguaje con definiciones, axiomas y reglas explícitas.
Es una diferencia crucial para leer titulares sobre «IA que resuelve matemáticas». Hay al menos tres niveles distintos:
- Generar una idea o una construcción: proponer una ruta que podría conducir a un resultado.
- Formalizarla: convertir los pasos en un lenguaje que un asistente de demostración pueda revisar.
- Aceptar el resultado: comprobar que responde a la pregunta correcta, entender sus ideas y someterlo al criterio de otros especialistas.
Qué comprueba Lean y qué no
Lean puede comprobar mecánicamente que los pasos formalizados se siguen de las definiciones, axiomas y supuestos codificados. Esa propiedad reduce el riesgo de errores dentro del desarrollo formal: si una inferencia no encaja con las reglas introducidas, el sistema la rechaza.
Pero Lean no decide por sí solo si se formalizó la pregunta matemática adecuada. Tampoco sustituye la interpretación de las ideas, la revisión del alcance de las hipótesis ni la valoración de la importancia del resultado. Un código correcto puede verificar una afirmación distinta de la que el lector cree que se ha demostrado si las definiciones o condiciones no coinciden.
Por eso una formalización es una pieza muy valiosa del proceso, no el proceso completo. La comunidad todavía necesita reconstruir el argumento, discutir sus supuestos y establecer qué se ha demostrado exactamente.
La presión sobre los matemáticos humanos
Steven Strogatz describió esta tarea de interpretación como «digestión de demostraciones»: explicar los argumentos generados por máquinas en términos que las personas puedan entender y valorar. En su opinión, los expertos humanos siguen aportando ahora la lectura contextual y el criterio necesarios para distinguir una cadena formalmente válida de una contribución matemáticamente significativa.
También advirtió de que la investigación podría volverse difícil de competir sin IA para quienes aspiren a trabajar en la frontera del campo. No es una predicción de desaparición de los matemáticos, sino una preocupación sobre cómo cambiarán las reglas de acceso al trabajo más avanzado.
Alex Townsend expresó una inquietud más personal. Después de 15 años dedicados a la investigación matemática, dijo sentirse amenazado al percibir que un sistema podía superar su nivel máximo de capacidad investigadora. La misma herramienta que puede hacer viable una tarea difícil también puede alterar la sensación de autoría y dominio profesional.
Ahí aparece el coste menos visible de estos avances. Si una máquina genera miles de rutas y otra persona solo selecciona, corrige o explica la mejor, seguirá siendo necesario decidir quién tuvo la idea, quién entendió el mecanismo y qué tipo de mérito corresponde a cada intervención.
El crédito sigue siendo una cuestión delicada
La llegada de OpenAI a este problema coincidió con trabajos relacionados de Tristan Buckmaster y Levent Alpöge sobre ecuaciones de fluidos. Las cuestiones de prioridad, reconocimiento y relación entre las distintas líneas de trabajo han sido objeto de posiciones enfrentadas. El 10 de septiembre, OpenAI afirmó que su investigación descartaba que los prompts de Codex de Buckmaster de los dos meses anteriores hubieran influido en ese sistema, incluso mediante el entrenamiento. Esa es la conclusión comunicada por la empresa, no una resolución independiente de la disputa.
Eso no permite afirmar que existiera un acceso indebido a trabajo privado ni resolver quién tuvo prioridad sobre una idea concreta. Sí permite identificar un problema general: cuando una empresa puede explorar muchas rutas con sistemas de IA y anunciar resultados a gran velocidad, la explicación pública puede adelantarse a la comprensión compartida.
En matemáticas, el crédito no consiste únicamente en publicar primero. También incluye reconocer los antecedentes, explicar qué parte de la estrategia es decisiva y permitir que otros especialistas comprueben si dos resultados realmente tratan el mismo problema.
La próxima prueba será entender el resultado
Los avances de septiembre de 2026 muestran una aceleración real de dos tareas diferentes: buscar construcciones matemáticas y convertir pruebas en código formal. OpenAI presentó una afirmación ambiciosa sobre Navier–Stokes que aún debe ganarse la aceptación independiente; Anthropic presentó una formalización de matemática establecida, no un descubrimiento de Fermat.
Para el lector, la regla útil es sencilla: no basta con preguntar si una IA «resolvió» un problema. Hay que preguntar qué problema, bajo qué condiciones, si el resultado es nuevo o una formalización y quién puede explicar sus pasos sin esconderse detrás del archivo de código.
La frontera decisiva no será solo producir demostraciones más deprisa. Será conseguir que otros matemáticos puedan reconstruirlas, discutirlas y reconocer con precisión qué se ha demostrado. En ese trabajo de comprensión, la intervención humana sigue siendo el criterio que separa una salida impresionante de un avance matemático aceptado.
