google-deepmind / google-deepmind/formal-conjectures
Erdős Problem 956
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 327
Description
### What is the conjecture
https://www.erdosproblems.com/956
If $C,D\subseteq \mathbb{R}^2$ then the distance between $C$ and $D$ is defined by
$$\delta(C,D)=\inf_{\substack{c\in C\\ d\in D}}\| c-d\|.$$
Let $h(n)$ be the maximal number of unit distances between disjoint convex translates. That is, the maximal $m$ such that there is a compact convex set $C\subset \mathbb{R}^2$ and a set $X$ of size $n$ such that all $(C+x)_{x\in X}$ are disjoint and there are $m$ pairs $x_1,x_2\in X$ such that
$$\delta(C+x_1,C+x_2)=1.$$
Determine $h(n)$ - in particular, prove that there exists a constant $c>0$ such that $h(n)>n^{1+c}$ for all large $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
Contributor guide
Assessment
This issue has not been assessed yet.