Essentially the same way we reason about infinite mathematical structures in our heads: we define infinite structures by a finite system of generators and prove things by induction. The computer verifies that your inductive proof is correct.