Hence, any proof checker will have statements it can't handle.

There are many things wrong with many of your statements here, but this one is particularly simple. You simply misunderstand what a proof checker does.

A proof checker does not deal with statements, it deals with formal proofs. Proof checking is roughly as complicated as parsing a context free language. That is, it is almost a trivial task.

Proof finding is another matter. A proof finder (aka a "theorem prover") takes a statement as input and attempts to produce a proof as output. Godel shows that there are statements that a proof finder can't handle.

You have repeatedly made claims which only make sense if you have the two kinds of programs confused. Fix that confusion, please.