A Lean 4 formalization of ten-pin bowling, including a model of frames and scoring rules, with formal proofs of properties such as the maximum possible score being 300.