I’ve seen ‘they run for some large amount of time/possible proofs, then they switch to their codepath for no proof found’
Sure… in which case there’s a third option, where they there is no proof that they cooperate/don’t cooperate with themselves precisely because they have limited runtime and so stop looking at proofs ‘prematurely’.
(So, for instance, there might be a proof that an agent that searched for 22000 clock cycles would cooperate with itself, and so it satisfies Lob’s Theorem… but no easier-to-find proof.)
Your quoted bit about Lob’s Theorem says nothing about how complex said proof will be.
Sure… in which case there’s a third option, where they there is no proof that they cooperate/don’t cooperate with themselves precisely because they have limited runtime and so stop looking at proofs ‘prematurely’.
(So, for instance, there might be a proof that an agent that searched for 22000 clock cycles would cooperate with itself, and so it satisfies Lob’s Theorem… but no easier-to-find proof.)
Your quoted bit about Lob’s Theorem says nothing about how complex said proof will be.