—

signature

reviewer:erdos-db-trust · no key registered on this bundle

✓

chain

null → 34d19d84

—

witness

no verifier attachment on record for this target

—

grade

in state · unreviewed

timeline

1. 2026-05-30proposeproposed · finding.addagent:erdos-spine-ingestvpr_41b7d4a92fab66ecCandidate claim vc_c037e200eba3c525 imported from artifact packet cap_61973ee16b553d57
2. 2026-05-30acceptfinding.assertedreviewer:erdos-db-trustnull→34d19d84vev_e60998de9e9b5ceaCandidate claim vc_c037e200eba3c525 imported from artifact packet cap_61973ee16b553d57

Erdős Problem #659 has status 'proved (lean)'. 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}}$? There does exist such a set: a suitable truncation of the lattice $\{(a,b\sqrt{2}): a,b\in\mathbb{Z}\}$ suffices. This construction appears to have been first considered by Moree and Osburn \cite{MoOs06}, who proved that it has $\ll \frac{n}{\sqrt{\log n}}$ many distinct distances. This construction was independently found by [Lund and Sheffer](https://adamsheffer.wordpress.com/2014/07/16/point-sets-with-few-distinct-distances/), who further noted that this configuration contains no squares or equilateral triangles. There are only six possible configurations of $4$ points which determine only $2$ distances (first noted by Erdős and Fishburn [ErFi96]), and five of them contain either a square or an equilateral triangle. The remaining configuration contains four points from a regular pentagon, and Grayzel [Gr26] (using Gemini) has noted in the comments that this configuration can also be ruled out, thus giving a complete solution to this problem. Boris Alexeev provides a formalisation of the reduction, which is conditional on Bernays' theorem (assumed as an axiom in the proof to obtain the $O(n/\sqrt{\log n})$ bound). See the [formal proof](https://github.com/plby/lean-proofs/blob/226d5fad7143dcebea2bbb5ec87f18a3a1dcea69/src/v4.24.0/ErdosProblems/Erdos659.lean). Topics: geometry, distances. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: possible.