Asistentes de prueba basados en LLM aceleraron bibliotecas Lean; matemáticos adoptaron flujos híbridos humano–máquina.
El ecosistema Lean 4, con mathlib y LLMs autoformalizadores, bajó la fricción de escribir pruebas chequeables por máquina.
Papers empezaron a incluir artefactos formales. La cultura cambió: “demostrado” puede significar también “verificado en Lean”.
Esa infraestructura es indispensable para evaluar anuncios espectaculares en 2026 sobre problemas del milenio.
Antes del anuncio de OpenAI, programas analíticos sobre singularidades y blow-up forzado en ecuaciones de fluidos ya empujaban la frontera.
Desde 2000, el Clay Mathematics Institute lista siete problemas; Navier–Stokes existence and smoothness es uno de ellos, con premio de un millón de dólares.
En septiembre de 2026 el anuncio de agentes OpenAI sobre Navier-Stokes reabrió el debate de crédito con el trabajo de Buckmaster y Alpoge en Euler; la verificación Clay/Millennium sigue en curso y OpenAI dijo no reclamar el premio.