What I don’t get about it is why you specify that the predictor computes proofs up to length N, and then just say how the predictor will do its proof.
If the outlined proof is less than N symbols long (which is true if N is large enough), the predictor will find it because it enumerates all proofs up to that length. Since the predictor’s proof system is consistent, it won’t find any other proofs contradicting this one.
The N < M is necessary to guarantee that the agent predicts the predictor’s proof, right?
Yeah. Actually, N must be exponentially smaller than M, so the agent’s proofs can completely simulate the predictor’s execution.
What happens if the outlined proof is more than N symbols long?
No idea. :-) Maybe the predictor will fail to prove anything, and fall back to filling only one box, I guess? Anyway, the outlined proof is quite short, so the problem already arises for not very large values of N.
If the outlined proof is less than N symbols long (which is true if N is large enough), the predictor will find it because it enumerates all proofs up to that length. Since the predictor’s proof system is consistent, it won’t find any other proofs contradicting this one.
The N < M is necessary to guarantee that the agent predicts the predictor’s proof, right?
What happens if the outlined proof is more than N symbols long?
Yeah. Actually, N must be exponentially smaller than M, so the agent’s proofs can completely simulate the predictor’s execution.
No idea. :-) Maybe the predictor will fail to prove anything, and fall back to filling only one box, I guess? Anyway, the outlined proof is quite short, so the problem already arises for not very large values of N.