La publicación de Navier-Stokes de OpenAI incluyó una demostración formal en Lean 4
La supuesta resolución por OpenAI de un problema del Premio del Milenio de Navier–Stokes usando “enjambres de agentes” de un modelo de lenguaje grande y una prueba formal en Lean 4 está generando tanto asombro como escepticismo. Los comentaristas ponderan la hazaña técnica y la promesa de la formalización automática de pruebas frente a los enormes costes de cómputo, las dudas sobre si la IA plagiaba o dependía en exceso del trabajo de investigadores humanos, y el riesgo de que las matemáticas se conviertan en algo que las máquinas hacen sin mejorar la comprensión humana. Muchos también examinan cuánto confiar en herramientas de verificación formal como Lean, qué errores o especificaciones incorrectas aún podrían invalidar los resultados, y si este tipo de pruebas de existencia negativas tienen aplicaciones físicas reales.
Coste y eficiencia de la formalización por IA frente a la humana
- El hilo cuestiona la afirmación de “cuatro órdenes de magnitud” de ahorro: estimaciones rápidas sugieren ~40 millones de dólares en cómputo frente a ~130 millones en trabajo humano, todavía enorme pero con una brecha menor.
- Algunos sostienen que el clásico “40 horas por página” para la formalización está obsoleto debido a una mejor automatización y a las bibliotecas; otros lo defienden para material complejo de nivel de investigación.
- Coordinar ~1 millón de horas de esfuerzo humano se considera prácticamente imposible en comparación con un gran enjambre de agentes.
Lean, autoformalización y rendimiento
- Muchos señalan que Lean moderno + mathlib reducen drásticamente el esfuerzo para material de nivel universitario, pero las demostraciones de investigación profunda siguen requiriendo un trabajo enorme.
- Se considera que Lean es lento a esta escala (por ejemplo, verificación de varios días y 230 GB), aunque varios apuntan que la generación con agentes funcionó masivamente en paralelo mientras que la verificación probablemente fue en su mayor parte en una sola máquina.
- Se discute la optimización del kernel de Lean y la demostración de que las versiones optimizadas son equivalentes a la simple; se mencionan proyectos que reimplementan Lean en Lean como una vía.
Verificación, confianza y posibles errores
- Consenso: si los axiomas y los enunciados de los teoremas son correctos, una prueba verificada en Lean es altamente fiable; el principal riesgo es formalizar mal el enunciado, no los pasos internos de la prueba.
- Algunos señalan que Lean ha tenido errores de kernel en el pasado; una IA, en principio, podría explotar un fallo así en lugar de demostrar realmente el teorema.
- Preocupa la posibilidad de formalizaciones “adversarias” que cambien sutilmente las definiciones; comprobar el enunciado del teorema y los supuestos sigue siendo responsabilidad humana.
Ética, plagio y uso de datos
- Gran subhilo sobre si las ideas clave de la IA fueron “plagiadas” de investigadores que usaron modelos anteriores, especialmente mediante entrenamiento con chats privados.
- Una postura: la cronología y las variantes del problema sugieren que la IA resolvió casos más difíciles y que el trabajo privado reciente no pudo estar en la ejecución de entrenamiento.
- La otra postura: la anonimización y la mezcla de datos de usuarios hacen “imposible saber” qué influyó en el modelo; la desconfianza hacia la ética del laboratorio amplifica las sospechas.
Importancia, comprensión y valor
- Algunos se asombran de que un modelo general pueda tanto resolver como verificar formalmente un problema así; otros temen que el resultado sea “un bit de información” con poca comprensión humana asociada.
- Se critica que los grandes laboratorios de IA busquen titulares, no una exposición matemática profunda, y que no respondan a preguntas de seguimiento ni se integren con la comunidad matemática más amplia.
Impacto práctico del resultado de Navier–Stokes
- Debate sobre la relevancia en el mundo real: algunos creen que este resultado negativo muestra principalmente que Navier–Stokes es un modelo físico imperfecto; otros ven aplicaciones inmediatas limitadas.
- Comparación con ejemplos paradójicos o muy artificiosos en matemáticas puras; escepticismo sobre si tales singularidades importan para la ingeniería o el modelado de turbulencia.
Reflexiones más amplias sobre IA y matemáticas
- Emociones mezcladas: entusiasmo por la autoformalización y por futuros trabajos en problemas como la conjetura abc, pero también ansiedad por que la creatividad matemática humana se esté “mecanizando”.
- Preocupación por futuras pruebas generadas por IA que los humanos no puedan comprobar de forma factible sin un enorme cómputo, y por posibles ataques a las cadenas de herramientas de verificación formal.