The problem addressed comes from Sipser's Introduction to the Theory of Computation: proving that language B is regular, where B consists of strings over an alphabet of three-bit columns. A string belongs to B if, when each row is read as a binary number, the bottom row equals the sum of the top two rows. For example, the column string [0,1,1] [0,0,1] [1,0,0] is in B because binary 3 + 1 = 4, but [0,1] [0,0] [1,1] is not since 1 + 0 ≠ 3. A language is regular if some deterministic finite automaton (DFA) accepts exactly its strings, meaning recognition requires only fixed memory regardless of input length.
The solution leverages the insight that while B itself is not directly recognizable left-to-right with fixed memory, its reversal B^R is. By processing the string from right-to-left (least significant bit first), the machine needs only to track the carry from binary addition. The adder DFA has three states: Carry 0 (both start and accepting state, indicating no overflow), Carry 1 (indicating a pending carry), and Dead (a sink state entered when the sum bit does not match the expected value from x_i + y_i + carry_in). Transitions are labeled with three-bit column symbols; solid arrows indicate valid transitions where the sum bit checks out, while dashed red arrows mark transitions where the sum bit fails and route to the Dead state. For instance, reading columns (1,1,0), (1,0,0), (0,0,1) from Carry 0 passes through Carry 1 twice and ends in the accepting Carry 0 state, confirming the reversed string is in B^R and thus the original string is in B. Conversely, the string (1,0,1), (0,0,1) starting from Carry 0 remains in Carry 0 after the first column but transitions to Dead on the second column when 0+0+0 produces sum bit 0 but the input claims 1, correctly rejecting the string.
This approach was formalized in Lean using Mathlib's library for formal languages and DFAs. The proof consists of three coordinated components: a precise specification of language B using set-builder notation over the alphabet Σ₃; an executable implementation of the adder DFA defining its states, transition function, and acceptance conditions; and a proof that the implementation matches the specification by establishing a run invariant connecting the automaton's carry state to the arithmetic sum. Mathlib provided essential support, including the theorem that regular languages are closed under reversal, allowing the proof to conclude B is regular once B^R was shown to be recognized by the DFA. The encoding demonstrates how constructive proofs in theorem provers mirror software development, with specifications corresponding to requirements, implementations to code, and verification proofs to test suites, offering software engineers concrete insight into the mechanics of formal verification.