Unit-distance bound below n^(4/3) claimed (OpenAI, Lean)

Your AI and this story

Key facts

• Manuscript (abstract, verbatim): ‘We prove a power saving for the planar unit-distance problem: for some absolute β < 4/3, every set of n points in the Euclidean plane determines O(n^β) unordered pairs at unit distance.’ Theorem 1.1: absolute constants 0 < C < ∞ and 1 ≤ β < 4/3 with u(n) ≤ C·n^β for every n. 53 pages, dated 23 Sept 2026
• Background (paper): Erdős posed the problem in 1946 with the lattice lower bound n^(1+c/log log n); Spencer, Szemerédi and Trotter proved u(n) = O(n^(4/3)) in 1984, reproved by Székely’s crossing-number method; Pach, Raz and Solymosi obtained a logarithmic improvement conditional on a rigidity conjecture. In May 2026 an OpenAI construction disproved Erdős’s conjecture u(n) = n^(1+o(1)) (see OpenAI model disproves Erdős’s 80-year-old unit distance conjecture); Sawin sharpened it to n^1.014114, and later work pushed the lower exponent to about 1.043
• Companion (abstract, verbatim): ‘We prove the weak pinned Erdős distinct-distance conjecture. For every fixed ε > 0, all but o(n) points of any n-point planar set determine at least n^(1−ε) distinct nonzero distances.’ 27 pages; Bloom lists it under Erdős problem #604
• Lean (OpenAI scope note lean/docs/167.md): ‘there are absolute constants C>0 and 1≤β<4/3 such that every finite planar point set of size n determines at most Cn^β unordered unit-distance pairs. The same constants work for every n’; the pinned-distance statement is a separate challenge. Both ‘accepted’ in the oai-math-revised comparator run of 25–26 Oct
• Thomas Bloom (erdosproblems.com, problem #90, 8 Oct): ‘The best lower bound for this problem, obtained by OpenAI in May, is n^{1+c} for some constant c>0. The best upper bound previously, due to Spencer, Szemerédi, and Trotter [SST84], was n^{4/3}. The PDF gives no indication as to the value of c obtained.’ The proof ‘appears to begin with a point-circle incidence interpretation (which was used in [SST84]), and couples that with some kind of entropy-based argument together with input from algebraic number theory’
• Expert reading (forum comment by WillSawin, 25 Oct): ‘The biggest progress is that I see how to remove the argument with ultrafilters from section 8, which was one of the things making the argument ineffective, and replace it with in-principle effective algebraic geometry reasoning.’ He describes the strategy as extracting structure from near-extremal configurations of the n^(4/3) argument and deriving a contradiction ‘in a somewhat surprising way’, with a key role for the Weil height of ratios on unit circles, and says of the entropy step: ‘I don’t understand this’
• Recognition of the bound: teorth/optimizationproblems PR #204 (merged by teorth on 18 Oct) adds ‘OpenAI, A power saving for planar unit distances’ as the source of the upper exponent 4/3 − ε with ε not explicit, and corrects ‘The comment saying the exponent 4/3 had not been improved’. Gil Kalai’s 7 Oct post lists the improved planar unit-distance bound among the release’s results