Lean 4 formalization of the Luby sequence, offering recursive, tree, and state-machine characterizations, proofs and lemmas.