[tombert]

Interesting, I hadn't heard this one.

I should see if I can model this in Isabelle or something and see what happens.

[7373737373]

for reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/e...