OpenAI publicó una demostración matemática que resuelve una cuestión pendiente sobre las ecuaciones de Navier-Stokes, pero el aspecto más relevante de su trabajo no ha recibido atención: la compañía presentó simultáneamente una prueba formal en Lean 4. Hasta hace poco, elaborar demostraciones formales verificables por máquina era un proceso extremadamente costoso: la regla empírica habitual, según Henk Barendregt y Freek Wiedijk en 2005, era de unas cuarenta horas de trabajo por página de libro de texto universitario. Aplicando esa estimación al artículo de 166 páginas de OpenAI, la formalización habría requerido alrededor de 132.800 horas-persona; sin embargo, la verificación en Lean se completó en solo 17 horas, una reducción de costes de cuatro órdenes de magnitud.
Esta drástica bajada del coste hace viable la verificación formal en campos donde antes resultaba prohibitiva. El autor del artículo señala que ya la ha empleado para validar pequeños textos propios y la considera una herramienta cotidiana. Entre las aplicaciones prácticas figuran la verificación de la coherencia de políticas de seguridad, la comprobación de que un contrato inteligente impone una responsabilidad máxima determinada, o la validación de algoritmos críticos en misiones industriales, problemas cuya formalización es más sencilla que la de las matemáticas de investigación y cuyo retorno de inversión resulta más fácil de cuantificar.