Científicos hallan discrepancias en la prueba en Lean de OpenAI sobre Navier-Stokes

Un grupo de científicos contrastó la prueba publicada por OpenAI sobre las ecuaciones de Navier-Stokes con su versión formalizada en Lean y encontró discrepancias en varios puntos clave. En esos puntos, la versión verificable por máquina demuestra enunciados más débiles que los que se declaran en el texto para humanos. Las ecuaciones de Navier-Stokes figuran entre los siete «problemas del milenio» del Instituto Clay de Matemáticas, cada uno dotado con 1 millón de dólares, así que cualquier grieta en un resultado de este tipo se nota de inmediato. Por ahora, esto no es una refutación.

Qué se ha descubierto exactamente

La verificación es sencilla. Se toma el artículo con la prueba y, en paralelo, una versión formal escrita en Lean, es decir, en un lenguaje donde un ordenador comprueba cada paso del razonamiento. Si ambas versiones describen lo mismo, coinciden. Aquí no coinciden: en varios puntos nodales, la versión en Lean afirma menos que el texto.

La descripción de la verificación no aclara si el trabajo de OpenAI aspira a resolver por completo el problema del Instituto Clay o solo a un resultado más acotado. El alcance de la afirmación debe juzgarse por la propia publicación, y es una salvedad importante. Pero la conclusión no cambia: el artefacto formal debe corresponderse con lo que se promete en el artículo.

Por qué un «enunciado más débil» es grave

Lean no admite argumentos del tipo «es evidente» o «se sigue de consideraciones estándar». Si una prueba supera la verificación, es correcta respecto a lo que exactamente está escrito en la formalización. Por eso la cuestión clave es si la versión formal demuestra lo mismo que se afirma con palabras. Cuando el enunciado en el código es más débil que el del artículo, caben varios escenarios:

• los formalizadores simplificaron las condiciones para llegar hasta el final y no lo dijeron;
• el texto formula la teorema de forma imprecisa, y la versión en Lean muestra lo que realmente se logró demostrar;
• un paso que en el artículo parece demostrado no se sostiene ante una verificación estricta;
• la discrepancia se debe a un desajuste técnico entre definiciones, que se resuelve con una corrección.

La primera y la cuarta opción son inofensivas; la tercera es peligrosa. Mientras los autores o expertos independientes no analicen cada punto por separado, no se puede elegir entre ellas.

Hechos clave con los datos disponibles:

• objeto de la verificación: la prueba de OpenAI sobre las ecuaciones de Navier-Stokes;
• método: comparación del texto publicado con la versión algorítmica en Lean;
• resultado: discrepancias en varios puntos clave;
• naturaleza de las discrepancias: en la versión para máquinas los enunciados son más débiles;
• estado: todavía no es una refutación, sino un motivo de duda.

Qué conviene vigilar

Si sigues la IA aplicada a las matemáticas, conviene tener presentes varias referencias. La primera es la reacción de OpenAI. Un análisis claro de cada discrepancia, ya sea una formulación corregida, un código en Lean actualizado o el reconocimiento de limitaciones, dirá más que cualquier declaración general. La segunda es lo que digan los especialistas en dinámica de fluidos y ecuaciones en derivadas parciales. La verificación formal comprueba la lógica, pero solo los matemáticos del área podrán evaluar si por el camino se perdió el sentido del problema. La tercera es si se publicarán la formalización y los materiales complementarios, de modo que la verificación pueda reproducirse de forma independiente.

Para quienes toman decisiones a partir de este tipo de anuncios, la conclusión es práctica. Un resultado de IA en matemáticas debe considerarse confirmado cuando existe una verificación independiente y la versión formal coincide con el teorema declarado. Un comunicado de prensa y un preprint no bastan. Mientras las discrepancias sigan abiertas, el caso de Navier-Stokes seguirá siendo una afirmación sonada, no un hecho aceptado.