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?
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.
Some people on LW have expressed interest in what's happening on the decision-theory-workshop mailing list. Here's an example of the kind of work we're trying to do there.
In April 2010 Gary Drescher proposed the "Agent simulates predictor" problem, or ASP, that shows how agents with lots of computational power sometimes fare worse than agents with limited resources. I'm posting it here with his permission:
About a month ago I came up with a way to formalize the problem, along the lines of my other formalizations:
Also Wei Dai has a tentative new decision theory that solves the problem, but this margin (and my brain) is too small to contain it :-)
Can LW generate the kind of insights needed to make progress on problems like ASP? Or should we keep working as a small clique?