I would say that "I am surprised that the bots have not been submitted to a PD tournament" but then I saw the paper was published in May and that's less than 6 months ago so instead I'll make the (silly, easy-to-self-fulfill) prediction that many or all of those bots will show up in the next PD tourney.

To the first point: I guess I'm not really comfortable with the proof of Theorem 4.1, per se, however the result seems incredibly intuitive to me. The choice of symbol/possible LaTeX error where one of the symbols is a square is confusing, and looking at it again three weeks later (I have not been on LW recently) I've forgotten too much of the notation to review it in depth in two to five minutes.

But I see Theorem 4.1 as the statement that "you can't stop someone from punishing you for something unless you think at a higher level than they do" and I assume that there exists a proof of that statement, and that the proof provided is such a proof.

I see Theorem 5.1 as saying that some set is compact for some reason and that implies existence of something for some reason, but I don't know why the thing is compact or why the desired object is the limit of the the things we constructed in the right way.

Although again it's been a while so I could be misremembering here.