He shows this by demonstrating a particular technique that can look at any formal system and build a statement that breaks it. Hence, any proof checker will have statements it can't handle.

He shows that for any given proof system, there exist statements for which no proof exists and no disproof exists either. That is not the same as breaking the proof-checker, which only cares about the particular proof it's given, not about whether other proofs or disproofs exist.

Proof generation is inherently complex. Proof verification is nearly trivial, and very well understood.