Green's Open Problems #86

### What is the conjecture
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.86

Let $c > 0$. Let $A$ be a set of $n$ (distinct) integers. Does there exist $\theta$ such that no interval of length $\frac{1}{n}$ in $\mathbb{R}/\mathbb{Z}$ contains more than $n^c$ of the numbers $\theta a \pmod{1}$, $a \in A$?

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-05

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading Green's Open Problems PDF, specifically problem 86, and inspect how related conjectures are represented in the formal-conjectures repository. Determine the appropriate Lean entry point for adding this statement and confirm that the conjecture is recorded in the repository's expected form.

Written by the indexing model from the issue text.