El problema abordado proviene de la Introducción a la teoría de la computación de Sipser: demostrar que el lenguaje B es regular, donde B consiste en cadenas sobre un alfabeto de columnas de tres bits. Una cadena pertenece a B si, al leer cada fila como un número binario, la fila inferior es igual a la suma de las dos filas superiores. Por ejemplo, la cadena de columnas [0,1,1] [0,0,1] [1,0,0] está en B porque binario 3 + 1 = 4, pero [0,1] [0,0] [1,1] no está ya que 1 + 0 ≠ 3. Un lenguaje es regular si algún autómata finito determinista (DFA) acepta exactamente sus cadenas, lo que significa que el reconocimiento requiere solo memoria fija independientemente de la longitud de la entrada.

La solución aprovecha la idea de que, aunque B mismo no es directamente reconocible de izquierda a derecha con memoria fija, su reverso B^R sí lo es. Al procesar la cadena de derecha a izquierda (bit menos significativo primero), la máquina solo necesita rastrear el acarreo de la suma binaria. El DFA sumador tiene tres estados: Acarreo 0 (estado inicial y de aceptación, indicando ausencia de desbordamiento), Acarreo 1 (indicando un acarreo pendiente) y Muerto (un estado sumidero que se entra cuando el bit de suma no coincide con el valor esperado de x_i + y_i + acarreo_entrada). Las transiciones están etiquetadas con símbolos de columnas de tres bits; las flechas sólidas indican transiciones válidas donde el bit de suma verifica correctamente, mientras que las flechas discontinuas rojas marcan transiciones donde el bit de suma falla y conducen al estado Muerto. Por ejemplo, al leer las columnas (1,1,0), (1,0,0), (0,0,1) desde Acarreo 0 se pasa por Acarreo 1 dos veces y se termina en el estado de aceptación Acarreo 0, confirmando que la cadena invertida está en B^R y, por lo tanto, la cadena original está en B. Por el contrario, la cadena (1,0,1), (0,0,1) partiendo de Acarreo 0 permanece en Acarreo 0 después de la primera columna pero transita a Muerto en la segunda columna cuando 0+0+0 produce un bit de suma 0 pero la entrada afirma 1, rechazando correctamente la cadena.

Este enfoque se formalizó en Lean usando la biblioteca de Mathlib para lenguajes formales y DFA. La prueba consta de tres componentes coordinados: una especificación precisa del lenguaje B usando notación de conjunto sobre el alfabeto Σ₃; una implementación ejecutable del DFA sumador que define sus estados, función de transición y condiciones de aceptación; y una prueba de que la implementación coincide con la especificación estableciendo una invariante de ejecución que conecta el estado de acarreo del autómata con la suma aritmética. Mathlib brindó soporte esencial, incluyendo el teorema de que los lenguajes regulares son cerrados bajo reversión, lo que permitió concluir que B es regular una vez demostrado que B^R es reconocido por el DFA. La codificación muestra cómo las pruebas constructivas en probadores de teoremas reflejan el desarrollo de software, con especificaciones correspondiendo a requisitos, implementaciones a código y pruebas de verificación a suites de prueba, ofreciendo a los ingenieros de software una visión concreta de la mecánica de la verificación formal.