Anatomy of a Lean Proof for Software Engineers

The piece proves that the language of height‑3 bit-columns where the bottom row equals the sum of the top two rows (viewing each row as a binary number) is regular. The alphabet consists of 3‑bit columns, so each string encodes three binary numbers column by column. The key insight is to reverse words so the DFA sees the least significant column first; that allows a finite automaton to check addition with constant memory by tracking only the carry. The constructive proof builds a DFA for the reversed language and then uses closure under reversal to obtain regularity of the original language.

The constructed adder DFA has three states: CARRY 0 (start and accepting), CARRY 1 (non‑accepting), and DEAD (sink). Transitions are determined by the full‑adder equations: sum bit = xi xor yi xor cin and carry_out = (xi∧yi) ∨ (cin∧(xi⊕yi)) - equivalently, whether at least two of xi, yi, cin are 1. Example runs show accepted and rejected inputs by how the carry propagates. The formalization in Lean uses Mathlib, establishes a run invariant by induction (base case, inductive step, run splitting), proves the DFA accepts the reversed language, and then applies reversal closure to conclude the original language is regular, illustrating how a straightforward textbook construction becomes a mechanized proof useful for software engineers.