Let’s say we are trying to prove statements within ZFC.
“ZFC can never prove this statement to be true”
...is one thing and...
“This proof checker can never prove this statement to be true”
...is another.
Neither can be proved by the specified proof checker—but the second statement can be proved by another, better proof checker—still working within ZFC—so it can be seen that it is true.
Let’s say we are trying to prove statements within ZFC.
“ZFC can never prove this statement to be true”
...is one thing and...
“This proof checker can never prove this statement to be true”
...is another.
Neither can be proved by the specified proof checker—but the second statement can be proved by another, better proof checker—still working within ZFC—so it can be seen that it is true.
“proved by a proof checker”—huh?
“Asserted”, “approved”—whatever.