Erdos Problem 1102

Stream: Formal conjectures

[Sham S]

https://github.com/google-deepmind/formal-conjectures/pull/1403 . I've created a pull request for Erdos 1102. But the formalization might contain error, I would be grateful if you can point out issues or any errors. Thanks, also the problem seems to be solved in this article by Dorn and Tao here.