Agost Biro turns a short textbook argument about regular languages into a complete Lean proof. The example is small—a finite automaton that checks binary addition—but it exposes the parts informal proofs usually skip.
The project separates three concerns:
- A specification: the bottom row of a three-row bit string equals the sum of the top two
- An executable DFA with only carry 0, carry 1, and a dead state
- A proof that the machine accepts exactly the specified language
The key move is reversing the input so the automaton reads least-significant bits first. That makes a single carry bit enough state for arbitrarily long inputs.
The first induction hypothesis is too weak because it describes only the final accepting case. The proof works after it records the boundary state on both sides of every partial run:
- Carry into the current word
- Carry out after the word
- The outgoing carry’s place value,
2 ^ word.length
That stronger invariant is the practical lesson. When a proof about a loop, parser, protocol, or state machine gets stuck, the desired end condition often omits information that must remain true between steps.
Formalization also surfaces a hidden requirement: equal row lengths leave nowhere to represent a final carry, so overflow must be rejected. The implementation is tiny; proving it matches the specification is where the system’s assumptions become visible.