El 19 de octubre de 2026, The Daily Californian publicó entrevistas en las que Richard Borcherds y Robin Huang, matemáticos de UC Berkeley, expresaron opiniones distintas sobre el papel de la inteligencia artificial en las matemáticas. El debate llega después de que un artículo técnico publicado el 6 de octubre señalara discrepancias entre partes de la prueba de Navier-Stokes de OpenAI y su formalización en Lean. Sus autores no concluyen que la prueba escrita sea incorrecta.
Dos visiones sobre la IA en matemáticas
Borcherds considera que, si el avance continúa, los investigadores humanos podrían volverse redundantes en pocos años. Huang, doctoranda de último año, cuestiona la utilidad actual de la IA para la investigación matemática y manifiesta preocupación por sus efectos en la comunidad y sus incentivos. Son perspectivas diferentes sobre una tecnología cuya capacidad investigadora también está en el centro de la controversia sobre Navier-Stokes.
Qué afirma OpenAI sobre Navier-Stokes
OpenAI anunció el 8 de septiembre que su sistema había obtenido un resultado para el problema de existencia y suavidad de las ecuaciones de Navier-Stokes en tres dimensiones. La empresa sostiene que un fluido incompresible, inicialmente en reposo y sometido a una fuerza externa suave, puede desarrollar una singularidad en tiempo finito, aunque conserve energía finita. OpenAI afirma que el resultado establece los enunciados C y D de la formulación del Clay Mathematics Institute. La explicación de OpenAI describe el resultado como una afirmación de la empresa.
NeoTeo ya había repasado los resultados matemáticos publicados por OpenAI a partir de un modelo interno. La cuestión técnica que centra ahora el escrutinio es más concreta: si la formalización en Lean refleja fielmente lo que dice la demostración escrita.
La discrepancia entre el texto y Lean
Lean es un asistente de demostración formal: permite codificar un enunciado matemático y los pasos de una prueba para que un sistema compruebe la demostración formalizada. En el artículo del 6 de octubre, A. Bastounis, F. Circelli y A. C. Hansen sostienen que algunas partes de la formalización de OpenAI no corresponden fielmente a pasajes de su prueba en lenguaje natural.
Un ejemplo aparece en una estimación de la sección 8.6. Los autores comparan el número de derivadas adicionales que requiere cada versión:
| Versión de la estimación | Derivadas adicionales |
| Texto en lenguaje natural | 4 |
| Estimación citada en Lean | 5 |
Los autores también analizan una estimación del flujo de presión y señalan diferencias entre las dos expresiones, que consideran difíciles de comparar. El artículo describe discrepancias concretas entre algunas partes de la formalización y el texto, no una conclusión de que toda la prueba escrita sea errónea. El análisis de A. Bastounis, F. Circelli y A. C. Hansen no afirma que la demostración en lenguaje natural de OpenAI sea incorrecta.
Qué comprueba una prueba formal
Lean comprueba la prueba tal como se ha codificado y el enunciado que esta pretende demostrar. Esa comprobación, por sí sola, no demuestra que el enunciado y los pasos codificados reproduzcan fielmente el argumento escrito en lenguaje natural. Esa diferencia entre comprobar una formalización y comprobar su correspondencia con el texto es el alcance del problema que plantean los autores.
