Leo de Moura: la IA ya escribe pruebas de 50 millones de líneas, pero verificar el código sigue siendo el cuello de botella
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Leo de Moura, creador de Lean y científico distinguido en AWS, explica cómo la IA está volviendo accesible la verificación formal. Con modelos capaces de traducir código de cualquier lenguaje a Lean, la atención se desplaza de escribir software a definir especificaciones y demostrar propiedades. Menciona casos como la biblioteca criptográfica SymCrypt de Microsoft y la prueba del último teorema de Fermat generada por Anthropic, y advierte que aún hay que comprobar que el modelo sea fiel al código real.
Ahora hay pruebas en Lean publicadas que tienen 50 millones de líneas. Mathlib tardó diez años, escrito por humanos, en pasar de cero a 2,5 millones. Y ahora hay gente escribiendo pruebas —con IA— de 50 millones de líneas.