we-solve (beta)

Math-567 · mathematics · Geometry

The Unit Distance Problem

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

For an $n$-point set $A\subset{\mathbb{R}}^2$, count unordered pairs of distinct points at Euclidean distance one. Define $u(n)=\max_{|A|=n}\#\{\{x,y\}\subseteq A:\|x-y\|_2=1\}$. No general-position assumption is imposed. This counts pairs at one prescribed distance, not the number of distinct distances. [S1] [S2]

Statement recorded in the supplied source.
What is the maximum number of unit distances determined by $n$ points in the plane? [S1]

Short English statement

What is the greatest number of pairs exactly one unit apart that n distinct points in the plane can determine?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-567-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-567

Planar unit-distance power saving: The bound u(n)<=C n^beta with beta<4/3 is an improved planar upper bound, not the conjectured n^(1+o(1)) order, an exact extremal value, or the other bundled dimension/distance questions.

This page records partial support. Complete resolution of the catalogue question is not established by this record.

The Unit Distance Problem

OpenAI's claim

Planar unit-distance power saving: The unit-distance manuscript claims an absolute exponent $\beta<4/3$ bounding the number of unordered unit pairs by $C n^\beta$. The point configuration is otherwise arbitrary.

Mathematical statement of the claimed result

Mathematical claim 1.
For $P\subset\mathbb R^2$ of $n$ distinct points let $u(P)$ count unordered pairs at Euclidean distance $1$, and let $u(n)=\max_{|P|=n}u(P)$. The claim is that absolute constants $C<\infty$ and $1\le\beta<4/3$ satisfy \[u(n)\le Cn^\beta\quad(n\ge0).\] The unspecified saving $4/3-\beta>0$ improves the known exponent but does not establish every proposed near-linear bound.

Outline of the argument

Planar unit-distance power saving: A near-extremal incidence sequence is transferred to algebraic configurations and analyzed using distance identities over a negligible-height coefficient field. After differentiating those identities, valuations distinguish the individual radicands and allow independent square-root sign changes. One unused sign change contradicts the differentiated system; a separate exclusion of popular unit circles handles the possible square-class failure, preventing approach to exponent $4/3$.

Formal verification

Family 167 describes Lean coverage for the weak pinned-distance conclusion and the separate fixed-power unit-distance improvement.

Planar unit-distance power saving: The manuscript links PinnedDistances.lean (declaration OAI.WeakPinned.main), PlanarUnitDistances.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →