Comment by tombert
2 days ago
Interesting, I hadn't heard this one.
I should see if I can model this in Isabelle or something and see what happens.
2 days ago
Interesting, I hadn't heard this one.
I should see if I can model this in Isabelle or something and see what happens.
for reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/e...