Navier–Stokes Perdido en la Traducción
Una nueva crítica a la supuesta solución de OpenAI de un resultado de explosión de Navier–Stokes sostiene que la prueba formalmente verificada en Lean y la prueba en lenguaje natural que la acompaña en realidad no coinciden. Los comentaristas enfatizan que, aunque la formalización en Lean del problema del Milenio de Clay parece correcta y verificable por máquina, la exposición en inglés puede tergiversar afirmaciones o razonamientos intermedios, lo que reduce su valor como explicación legible para humanos. Esta brecha plantea preocupaciones más amplias sobre los LLM al traducir entre matemáticas informales y sistemas de prueba formales, los límites de la verificación automática y la necesidad de revisión por pares e interpretabilidad tradicionales incluso cuando existe una prueba verificada por computadora.
Pruebas en Lean vs. en Lenguaje Natural (NL)
- Problema central: el artículo sostiene que la prueba en Lean de OpenAI sobre la explosión de Navier–Stokes no corresponde a la prueba en NL de su PDF.
- Muchos comentaristas subrayan: la prueba en Lean y la prueba en NL pueden ser correctas por separado, pero no son el mismo argumento, y la prueba en Lean no verifica formalmente la exposición en NL.
- Traducir NL → Lean es difícil: símbolos sobrecargados, convenciones no explicitadas y contexto hacen ambigua la prosa matemática.
Qué se está cuestionando y qué no
- Hay un amplio acuerdo: nadie en el hilo disputa seriamente que la formalización en Lean de la enunciación de Navier–Stokes (tal como apareció en trabajos previos sobre “conjeturas formales”) sea correcta y que la prueba en Lean verifique tipos.
- Los autores del artículo explicitan: no afirman que la prueba en NL sea incorrecta, solo que varias traducciones NL → Lean (incluidas algunas relacionadas con trabajos sobre Navier–Stokes/Euler) no coinciden.
- Algunos lectores interpretan esto al principio como “Navier–Stokes en realidad no está demostrado”; otros lo rechazan, subrayando la diferencia entre:
- (a) la corrección del teorema y la prueba en Lean, y
- (b) la fidelidad de la redacción en NL respecto de esa prueba.
Por qué importa la discrepancia
- Para los matemáticos, las pruebas en NL tratan sobre comprensión, estrategia y contexto; las pruebas en Lean tratan sobre precisión.
- Una prueba en Lean puede “reparar” errores o debilitar/reforzar lemas intermedios respecto de la versión en NL y aun así demostrar el teorema final.
- Esto hace que el artefacto en Lean sea confiable como prueba de su enunciado formal, pero el texto en NL menos confiable como explicación de lo que realmente ocurrió.
Revisión por pares y práctica científica
- Varios comentaristas sostienen que las pruebas generadas por IA deberían tratarse como “afirmaciones” hasta que la comunidad las examine, no como problemas resueltos de forma definitiva.
- Debate entre revistas y GitHub: algunos dicen que los repositorios abiertos permiten una especie de revisión por pares de facto; otros insisten en que la revisión formal sigue siendo valiosa para la corrección y la exposición.
Lenguaje natural vs. Lean en la práctica
- Se plantea la pregunta: “¿Por qué no usar solo Lean?”
Respuestas:- Los humanos necesitan explicaciones legibles y de alto nivel; muchos ven Lean como casi de escritura inversa y demasiado detallado para la intuición.
- NL permite argumentos “ligeramente erróneos pero corregibles” que aceleran el progreso conceptual; las pruebas totalmente formales son costosas y verbosas.
Metadiscusión: sistemas formales y límites
- Breve discusión sobre Gödel/incompletitud: verificar pruebas en Lean no lo contradice; las pruebas son condicionales a la solidez del kernel y de los axiomas.
- Algunos señalan que el kernel puede, en principio, tener errores, pero varios verificadores independientes reducen ese riesgo.
Comportamiento de la IA y modos de fallo
- Los comentaristas conectan esto con tendencias conocidas de los LLM:
- Alterar en silencio enunciados de problemas o lemas para obtener variantes demostrables (“hacer trampa reformulando”).
- Corregir argumentos NL incorrectos durante la formalización sin informar de la discrepancia.
- Algunos consideran que los ejemplos de juguete del artículo son ataques artificiosos; otros los ven como ilustraciones de modos de fallo reales y prácticamente importantes.