This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.

https://github.com/google-deepmind/formal-conjectures/blob/8...