Claim. For a finite set $X\subset\mathbb{R}^2$ let $u(X)$ be the number of unordered pairs of distinct points of $X$ at Euclidean distance one, and let $u(n)$ be the largest $u(X)$ over sets of $n$ points; this is $f_2(n)$ of Problem 1085. Theorem 1.1 of the manuscript A power saving for planar unit distances of the OpenAI mathematics release, dated 23 September 2026 and authored by OpenAI (its intake card is openai_2026_power_saving_planar_unit_distances, with the theorem paged at Theorem 1.1), states that there are absolute constants $C>0$ and $1\le\beta<4/3$ such that

Equivalently $u(n)=O(n^{4/3-\delta})$ for an absolute $\delta>0$: a fixed power below the exponent $4/3$ of the bound of Spencer, Szemerédi and Trotter [SST84] recorded on the problem page. The constants $C$ and $\beta$ are existential; the manuscript gives no numerical exponent. Its introduction outlines the proof as a contradiction along a sequence of counterexamples: unit distances are read as incidences between the points and unit circles centered at a second copy of the set, random cuttings isolate a piece of the incidence graph with controlled degrees, an entropy bound shows that the two endpoints of a wedge share little information, a prediction lemma resamples a point from a short history of coordinate tests, the product formula for absolute values converts relations between the edge jumps into bounds on heights of algebraic numbers, and an algebraic obstruction rules out the dense graph of pairs that remains. The prose proof of Sections 2--8 is not reviewed. The manuscript itself places the theorem against the lower side, the lattice bound $n^{1+c/\log\log n}$ of Erdős and the fixed-power constructions along unbounded sequences of sizes recorded on the page of Problem 90, and notes the gap that remains between the two exponents. The problem is open because its planar and three-dimensional cases are: in the plane the exponent of $f_2(n)$ lies between $1$ and $\beta$ and no order of growth is determined, while in dimension four and above the literature recorded on the problem page and on the other claim pages of this folder determines $f_d(n)$ to within lower-order terms.

Covers. $f_2(n)\le Cn^{\beta}$ for some $\beta<4/3$ (planar upper bound only; no lower bound, nothing for $d\ge3$).

Depends on. No page of this wiki. The theorem is the manuscript's own, and the Lean development, forty modules under lean/OAI/Geometry/UnitDistances/, imports only Mathlib and its own files.

Formalization. The release's Lean tree at the pinned revision defines, in lean/OAI/Geometry/UnitDistances/Basic.lean, Plane as EuclideanSpace ℝ (Fin 2), IsUnitPair on Sym2 Plane as dist x y = 1, unitPairCount X as the number of members of X.sym2 that are unit pairs, and u n as the supremum in ℕ of the counts over finite sets of cardinality n; the file lean/OAI/Geometry/UnitDistances/Main.lean proves

theorem main : ∃ C β : ℝ, 0 < C ∧ 1 ≤ β ∧ β < (4 : ℝ) / 3 ∧
    ∀ n : ℕ, (u n : ℝ) ≤ C * (n : ℝ) ^ β

as OAI.PlanarUnitDistances.main. The statement is Theorem 1.1 literally: the diagonal of X.sym2 is excluded because dist x x = 0, the set of counts over n-point sets is nonempty and bounded by n ^ 2 (both proved in Basic.lean), so the ℕ-supremum is the true maximum and not the default value 0 of an unbounded supremum, the distance is Euclidean, and u n is $f_2(n)$. The comparator challenge lean/ComparatorChallenges/PlanarUnitDistances.lean, with its configuration PlanarUnitDistances.json, pins main with definitions identical to those of Basic.lean and permits only the axioms propext, Quot.sound and Classical.choice. The release's own catalog is inconsistent about this theorem: lean/formalization.yaml lists for the family only the weak pinned distance declaration OAI.WeakPinned.main, and lean/docs/167.md says the unit-distance theorem is not included and then describes it as formalized; the module is imported by the release's root file lean/OAI.lean and the challenge pins it, so the formalization exists and the catalog entry is what is wrong.

Acceptance. Formalized: this corpus's verification built OAI.PlanarUnitDistances.main at the pinned revision, found its axiom closure to be exactly propext, Classical.choice and Quot.sound, found the pinned comparator fingerprint identical, and audited the whole statement against the problem's statement as set out above. The acceptance is of the Lean statement so audited; the prose proof of the manuscript is not reviewed. Not reviewed and not refereed: no outside reviewer is recorded as having examined the result, and the site's page for Problem 1085, as accessed on 2026-09-04 and as last edited 23 May 2026, shows OPEN with no mention of the release. The release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification.