It seems to me that the variant with time limits has a simple quining solution:
1) Get the time limit as input.
2) Spend almost all available time trying to prove in some formal theory that the next program is equivalent to this one.
3) Double down if a proof is found, otherwise take winnings.
That’s similar to your idea, right? I’m not sure if it addresses Eliezer’s objection, because I no longer understand his objection...
That’s similar to your idea, right?
Yes.
It seems to me that the variant with time limits has a simple quining solution:
1) Get the time limit as input.
2) Spend almost all available time trying to prove in some formal theory that the next program is equivalent to this one.
3) Double down if a proof is found, otherwise take winnings.
That’s similar to your idea, right? I’m not sure if it addresses Eliezer’s objection, because I no longer understand his objection...
Yes.