The board / number theory / #466
Erdős Problem #466
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`N X δ` is the maximum number of points in a closed disc of radius `X` in the plane such that the distance between any two of them is at least `δ` away from the nearest integer.
Let \(N(X,\delta)\) denote the maximum number of points \(P_1,\ldots,P_n\) which can be chosen in a circle of radius \(X\) such that \[\| \lvert P_i-P_j\rvert \| \geq \delta\] for all \(1\leq i<j\leq n\). (Here \(\|x\|\) is the distance from \(x\) to the nearest integer.) Is there some \(\delta>0\) such that \[\lim_{X\to \infty}N(X,\delta)=\infty?\] Graham proved this is true, and in fact \(N(X,1/10)> \frac{\log X}{10}\). This was substantially improved by Sárközy [Sa76], who proved that for all sufficiently small \(\delta>0\), \(N(X,\delta)>X^{1/2-\delta^{1/7}}\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/466.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/466
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.