Comment by QuadmasterXLII
3 months ago
Not quite. There is some N for which you can’t prove BB(N) is correct for any existing proof assistant, but you can prove that BB(N) by writing a new proof assistant. However, the problem “check if new sufficiently powerful proof assistant is correct” is not decidable.
No comments yet
Contribute on Hacker News ↗