Un artículo reciente publicado en arXiv argumenta que la verificación automática de pruebas matemáticas mediante el lenguaje de programación Lean no garantiza la validez de los argumentos originales expresados en lenguaje natural (NL). El texto, titulado 'Navier-Stokes lost in translation', analiza específicamente el proceso de autoformalización, donde sistemas de inteligencia artificial traducen textos matemáticos de NL a lenguajes formales como Lean para su verificación mecánica. El autor, Alexander Bastounis, sostiene que esta metodología carece de confianza en la integridad del razonamiento original debido a las dificultades inherentes en la traducción semántica fiel.
El artículo destaca que la resolución de ambigüedades en textos matemáticos de NL es un problema computacionalmente arbitrariamente difícil, situándose en la cima de la jerarquía de complejidad de Solvability (SCI), con un valor infinito. Esto implica que la autoformalización semánticamente fiel es más difícil que cualquier problema computacional, incluyendo el problema de la parada. Para ilustrar estas limitaciones, el autor presenta ejemplos prácticos de traducciones erróneas de IA que generan discrepancias entre las pruebas en NL y sus verificaciones formales en Lean. Un caso de estudio central es la prueba anunciada por OpenAI sobre el comportamiento de las soluciones de las ecuaciones de Navier-Stokes. El análisis demuestra que la prueba formalizada en Lean no corresponde a la prueba original en lenguaje natural, evidenciando que la verificación mecánica no valida automáticamente la lógica subyacente del texto original.