Erdős Problem 1066

### What is the conjecture

https://www.erdosproblems.com/1066

Let $G$ be a graph given by $n$ points in $\mathbb{R}^2$, where any two distinct points are at least distance $1$ apart, and we draw an edge between two points if they are distance $1$ apart.

Let $g(n)$ be maximal such that any such graph always has an independent set on at least $g(n)$ vertices. Estimate $g(n)$, or perhaps $\lim \frac{g(n)}{n}$.

Status: open

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

The issue names no repository file, test, or entry point; start by reading the Erdős Problems 1066 statement and examining nearby formalized conjectures in the repository. Done means the conjecture about independent sets in unit-distance graphs is added as a Lean formal statement following the project's conventions.

Written by the indexing model from the issue text.