Problem 659

../

claims/: The 3 claim pages of Problem 659, one per claimant's result; the problem's standing derives from them.

---

Statement. Is there a set of $n$ points in $\mathbb{R}^2$ such that every subset of $4$ points determines at least $3$ distances, yet the total number of distinct distances is

$$\ll \frac{n}{\sqrt{\log n}}?$$

Status. Proved. The site's label is PROVED (LEAN); the formalization that suffix marks assumes Bernays' theorem as an axiom, and this corpus has not built it, so no formalized evidence is credited.

Source. erdosproblems.com/659, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #659, https://www.erdosproblems.com/659.

References.

• [ErFi96] Erdős, Paul and Fishburn, Peter, Maximum planar sets that determine $k$ distances. Discrete Math. (1996), 115-125.
• [MoOs06] Moree, Pieter and Osburn, Robert, Two-dimensional lattices with few distances. Enseign. Math. (2) 52 (2006), 361-380.

Formalization. Statement in formal-conjectures.

Current assessment

• Status target and evidence. The standing in the frontmatter is derived from Grayzel's claim page, an accepted full claim that targets the exact planar existence question displayed above. Grayzel's Theorem 1 has the same quantifiers and bound. The public discussion records Bloom's mathematical confirmation, the reviewed evidence, and Tao's acceptance of the reported qualified formal verification, which the claim page records as a link and not as formal evidence.
• Current best progress. For every integer $n\geq2$, Grayzel constructs an $n$-point subset of $P_{\lceil\sqrt n\rceil}\subset\mathbb Z\times\sqrt2\mathbb Z$ with the required local property and $O(n/\sqrt{\log n})$ total distances. No stronger claim is needed for this question.
• Status and source search. The site snapshot was accessed 2026-09-04. arXiv:2601.09102v2 (16 January 2026) is the latest version (arXiv record, 2026-09-06). No broader literature or publication search is recorded here.
• Other claims. Feng and coauthors' report on the Aletheia research agent gives an independent proof of the same answer on the lattice of the ring of integers of $\mathbb Q(\sqrt{-7})$, generated before Grayzel's note was written; it is recorded as a claimed full claim on Feng and coauthors' claim page, since the site credits Grayzel. Sheffer's 2014 survey (source card) lists $\phi(n,4,3)=O(n/\sqrt{\log n})$ in its Table 3, the affirmative answer to this question, but its argument (p. 14) excludes only squares and uses the triangular lattice, which contains four-point two-distance sets made of two equilateral triangles; Terence Tao recorded the error on the discussion thread on 13 January 2026. The bound itself is true, since Grayzel's Theorem 1 proves it; only the survey's argument fails, and the survey's entry is recorded as a rejected claim.
• Proof coverage and review. The Grayzel source home contains complete own-words proofs of Theorem 1, Corollary 4, Theorem 5, and Lemmas 6--8. The exact scope, external premises, limitations, and current independent review state are recorded on Theorem 1.
• Remaining gaps and limits. Bernays' represented-integer asymptotic and Perucca's six-type classification are stated as precise external premises, not recursively proved. The reported Lean formalization assumes Bernays' theorem as an axiom, and no local Lean build or Mathlib-foundational proof is recorded. Publication status and historical priority are outside this proof reconstruction.

Progress

Grayzel's Theorem 1 answers the stated question affirmatively for every integer $n\geq2$. It constructs an $n$-point subset of a finite box in $\mathbb Z\times\sqrt2\,\mathbb Z$ satisfying both the four-point condition and the $O(n/\sqrt{\log n})$ distance bound. The selected source is Grayzel's paper (arXiv:2601.09102v2, 16 January 2026).

Thomas Bloom confirmed the mathematical solution on 13 January 2026 in the public discussion. On 14 January, Boris Alexeev reported an Aristotle formalization that assumes Bernays' theorem as an axiom; Terence Tao explicitly accepted that level of verification for the public record. The site's label PROVED (LEAN) therefore carries this external-theorem qualification here. No local Lean build or verification from Mathlib's foundational axioms alone is recorded here. The postings, the acceptance and the formalization's pinned location are on the claim page.

Known Results

Corollary 4 uses the positive definite binary quadratic form $u^2+2v^2$ and Bernays' represented-integer asymptotic to prove the global distance estimate. The choice $m=\lceil\sqrt n\rceil$ is essential: it keeps the containing box size $m^2$ comparable to $n$. The claim is not a bound for an arbitrary $n$-point subset of an arbitrarily larger box.

Theorem 5 proves the local condition from Perucca's exhaustive classification. Its three same-paper inputs exclude squares, equilateral triangles, and the regular-pentagon trapezoid from the anisotropic lattice.

Earlier anisotropic lattice distance counting appears in Moree-Osburn; the local four-point exclusion is an additional requirement.

The theorem matches the planar question here; it is not a theorem about vertices of three-dimensional convex polyhedra.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_fishburn_1996_maximum_planar_sets_that_determine_k_distances
• feng_2026_semi_autonomous_mathematics_discovery_gemini_case
• feng_2026_semi_autonomous_mathematics_discovery_gemini_case / solution_p24
• grayzel_2026_solution_problem_erdos_concerning_distances_points
• grayzel_2026_solution_problem_erdos_concerning_distances_points / corollary_4
• grayzel_2026_solution_problem_erdos_concerning_distances_points / lemma_6
• grayzel_2026_solution_problem_erdos_concerning_distances_points / lemma_7
• grayzel_2026_solution_problem_erdos_concerning_distances_points / lemma_8
• grayzel_2026_solution_problem_erdos_concerning_distances_points / theorem_1
• grayzel_2026_solution_problem_erdos_concerning_distances_points / theorem_5
• moree_2006_two_dimensional_lattices_few_distances
• moree_2006_two_dimensional_lattices_few_distances / theorem_1
• moree_2006_two_dimensional_lattices_few_distances / theorem_5
• sheffer_2014_distinct_distances_open_problems_current_bounds
• sheffer_2014_distinct_distances_open_problems_current_bounds / problem_29