{"id":"palomar/PALOMAR-2026-10-04-000008","url":"https://github.com/linrock/math-proofs/tree/2afe25fe500b036dfabef8e00c369a434bfff763/erdos-956","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000008-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.MG","math.CO","msc:52C10","msc:52A10","msc:05D99","discrete-geometry","erdos-problems","unit-distances","lean-formalization"],"score":0,"title":"Erdős 956: unit distances between disjoint convex translates","trust":"high","domain":"math.MG","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.MG","summary":"A complete Lean 4 proof of the affirmative answer to Erdős problem 956: for all sufficiently large n, there exist n pairwise-disjoint translates of a compact convex planar set with more than n^(1+c) unordered pairs at Euclidean set-distance 1 (for c = 1/4). Adapting the parabolic construction announced by Valtr (2005) and detailed in Chojecki's April 2026 manuscript, the formalization proves the supporting-hyperplane theorem for a centrally symmetric signed parabolic cap and constructs a four-layer parabolic grid of disjoint translates. This establishes the explicit lower bound h(n) > (1/26)…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"Erdős Problem 956","identifier":"https://www.ulam.ai/research/erdos956.pdf","relationship":"adapts"}]}