Colloquially, Godel's theorem says that for any formal system complex enough to implement a certain subset of mathematics there will be syntactically valid theorems that the system cannot evaluate. 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.

There's a lot to object to there, but let's be generous about "colloquially." Here is a more precise and correct rewording of your last line: "Any algorithm that takes a statement as input and searches for a proof or disproof will fail on some inputs." Here is a more precise and incorrect rewording: "There is no algorithm that takes a proof as input and evaluates the correctness or incorrectness of that proof."