A fully generalized automated "proof checking" is also impossible because it depends on what system of axioms and rules the checking algorithm is using, which i

A fully generalized automated "proof checking" is also impossible because it depends on what system of axioms and rules the checking algorithm is using, which is, again, limited by incompleteness theorems. BTW if we have a proof checking algorithm in some axiomatic system then it's pretty easy to write a proof finding algorithm in this system. Via a brute-force - it just checks all strings as a possible proofs of a statement and simultaneously all strings as a proof of negation. It will definitely stop if there is a proof of the statement or its negation, but will run infinitely if both proofs are missing.