Así se demuestra formalmente un DFA en Lean: el reto de verificar que la suma de dos filas de bits es regular
Anatomy of a Lean proof for software engineers
El autor formaliza en Lean un problema clásico de teoría de la computación: probar que el lenguaje de columnas de bits donde la fila inferior es la suma de las dos superiores es regular. Como un DFA lee de izquierda a derecha, construye un autómata que reconoce el lenguaje invertido y luego usa la propiedad de cierre del reverso. El artículo muestra paso a paso la especificación, la implementación y la prueba inductiva, ofreciendo a los ingenieros de software una idea concreta de qué implica verificar propiedades de un sistema con un asistente de pruebas.
El truco es recordar cómo sumas números a mano: trabajas desde el dígito menos significativo al más significativo. Lo único que arrastras de una columna a la siguiente es el acarreo.