No, but you hit the nail on the head, that’s the most interesting part.
The proof verifier uses fixed math axioms. The busy beaver function at high enough N cannot be proven with those axioms.
The proof verifier uses fixed math axioms. The busy beaver function at high enough N cannot be proven with those axioms.
"Everything that can be proven" is relative. PA can prove some things, ZF more things. In 200 years we could develop more powerful math foundations which can prove more things. Today's proof verifiers could never prove them, but tomorrow's proof verifiers could. And the cycle repeats.
This is quite simple. f(p) = C implies p does the job quite elegantly.
Interestingly it's harder to do the opposite, to simulate ZF in ZFC, because there is no way to express "forget that you know about C". Such a construction cannot be possible in general because if a contradictory axiom is added, then everything is true, and a theory where everything is true is useless and can't simulate anything. However for C in particular I believe it should be possible to make such a construction but I can't immediately think of how I would do it.