4 ms·
Interesting, I hadn't heard this one. I should see if I can model this in Isabelle or something and see what happens.
by tombert 1y ago
Interesting, I hadn't heard this one.
I should see if I can model this in Isabelle or something and see what happens.
- 7373737373 1y agofor reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/eda179635c14c1c9a0abb51843cd40e291b5c70b/FormalConjectures/Other/BeaverMathOlympiad.lean#L92 https://github.com/google-deepmind/formal-conjectures/blob/e...