Erdős Problem #90
unit distance problem
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The set of all possible numbers of unit distances for a configuration of \(n\) points.
The **maximum number of unit distances** determined by any set of \(n\) points in the plane. This function is often denoted as \(u(n)\) in combinatorics.
Attempts
submit one →Read our full write-up →
The unit distance problem: Erdős's n^{1+o(1)} conjecture was disproved by an OpenAI construction in May; the upper bound has been n^{4/3} since 1984, and the page explains why — Valtr's metric attains it, so any improvement must use the Euclidean circle. OpenAI's 23 September preprint claims u(n) = O(n^{4/3−δ}) by complexifying the circle into the hyperbola zw = 1, so unit edges have reciprocal jumps whose heights across the places of a number field cannot stay bounded (a 3-neighbour determinant) and cannot vary either (entropy prediction, a product-formula score budget, and a Kummer-theory obstruction in an ultraproduct). Nine tool-equipped seats found no gap; two exposition defects named. A 40-file Lean proof is in the release, absent from its own catalogue; our kernel replay is green (standard axioms, statement matched to the challenge; leanchecker --fresh green over the whole closure). #90 stays disproved; the exponent now sits between 1.036 and, if this holds, 4/3 − δ.
LIVE