{"id":"palomar/PALOMAR-2026-10-05-000004","url":"https://github.com/linrock/math-proofs/tree/08152671ab394392fd941b18654daba734c26518/erdos-958","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-05-000004-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.CO","math.MG","msc:52C10","msc:05D99","discrete-geometry","distance-distributions","erdos-problems","lean-formalization"],"score":0,"title":"Erdős 958: planar point sets with distance multiplicities {1, ..., n - 1}","trust":"high","domain":"math.CO","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 proof of the negative answer to Erdős problem 958: for every n ≥ 4, there exists an n-point configuration in the Euclidean plane determining n - 1 distinct interpoint distances with multiplicities {1, 2, ..., n - 1} that is neither equidistant on a line nor equidistant on a circle. Formalizing the May 2025 construction of Clemen, Dumitrescu, and Liu, the proof places n - 1 equally spaced points on a short arc of the unit circle together with the center (0, 0), uses strict monotonicity of chord lengths on [0, π/3) to compute the exact distance-multiplicity profile, and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-05","reactions":{},"formalized":true,"formalizes":[{"title":"On multiplicities of interpoint distances","identifier":"https://arxiv.org/abs/2505.04283","relationship":"formalizes"}]}