Green's Open Problems #76

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

Let $A$ be a set of $n$ points in the plane. Can one select a set $A'$ of $n/2$ points, with the property that any axis-parallel rectangle containing 1000 points of $A$ contains at least one point of $A'$?

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

* ams-52
* 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 with the linked Green's Open Problems PDF at problem 76, then inspect the formal-conjectures repository for the conventions used to add conjectures. Done means the stated plane-point conjecture is added to the repository in the project's Lean formalization style.

Written by the indexing model from the issue text.