A fixed positive power gain refutes the near-linear Euclidean conjecture in the cited proof and human companion exposition. Exact extremal growth remains a related research question.
Count unordered pairs of distinct points in the Euclidean plane at distance exactly one. Write u(n) for the maximum over all n-point sets. The conjecture asks that for every ε > 0, u(n) ≤ n^(1+ε) for all sufficiently large n. Determining the exact extremal growth remains a broader question.
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
Where the growth exponent lies
The true exponent θ is now known to lie strictly above 1 and at most 4/3. The 2026 gain δ is not explicit, so the open interval is drawn from 1, which is itself excluded. Erdős’s grid gives a gain c/log log n that tends to zero, which is why the conjecture θ = 1 was plausible.
Visual setup
What counts as one unit-distance pair?
A unit square has four distance-one pairs; its diagonals are longer. Each unordered pair is counted once.
Reading boundary. A drawing of four points does not demonstrate a fixed exponent gain or the asymptotic counterexample.
The square illustrates counting only. Select a statement for its exact scope and sources.
Text version
Four corner points form a square with its four sides highlighted. A dashed diagonal is excluded from the unit-pair count. This finite example introduces the quantity used in the asymptotic theorem.
The mathematical example is a unit square; the drawing coordinates are illustrative. Only distinct unordered Euclidean distance-one pairs count.
Read the counting convention
✕Disproved
The near-linear unit-distance conjecture
The near-linear asymptotic assertion is refuted; this does not determine the exact maximum.
Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.
An asymptotic construction, not a statement about every size or an explicit value of δ.
OpenAI 2026Formalized
Theorem · Counterexample
●ProvedOpenAI 2026
A fixed power gain for infinitely many sizes
There exists δ>0 such that for every N there are n ≥ N and a set of n distinct Euclidean planar points with at least n1+δ unordered unit-distance pairs.
Assumptions
Finite point sets in the Euclidean plane.
The same δ works along an unbounded sequence of sizes.
In this problem
An asymptotic construction, not a statement about every size or an explicit value of δ.
The square-grid intuition does not give the final growth law
Under stated assumptions
The fixed exponent gain rules out any upper estimate with an exponent tending to one. The remaining problem is to sharpen the extremal growth estimates.
Limit The original theorem does not provide the best possible exponent or certify the separately announced δ = 0.014 refinement.
Reported in sources: A pinned Lean submission reports the asymptotic counterexample with exact Euclidean pair counting. External execution and independent OpenMath review remain pending.
CComputation
None recorded
RReview
Not yet reviewed
OpenMath assessment: A fixed positive power gain refutes the near-linear Euclidean conjecture in the cited proof and human companion exposition. Exact extremal growth remains a related research question.
Source comparison and reader curation; independent mathematical assessment remains pending.
OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027
The finite-set definition counts ordered off-diagonal distance-one pairs and divides by two. The endpoint uses EuclideanSpace ℝ (Fin 2), not the product sup norm, and proves arbitrarily large sizes. It does not specify δ = 0.014.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Noga Alon · Thomas F. Bloom · W. T. Gowers · Daniel Litt · Will Sawin · Arul Shankar · Jacob Tsimerman · Victor Wang · Melanie Matchett Wood · Preprint · May 20, 2026
OpenAI’s unnamed internal model generated the original construction. The nine companion-paper authors provide human exposition and checking; Will Sawin’s announced exponent refinement has separate credit. The plby/Erdos90 project supplies the linked formal submission; its checked README does not identify an individual formalization author.
Research direction
Keep follow-up refinements separately credited
The announcement attributes a δ = 0.014 refinement to Will Sawin, separately from the original model-generated argument.
No exact formal target for that numerical refinement is claimed here.
Related statements · context, not additional proved progress