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

for 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...