The Erdős unit distance and pinned distance problems
The Erdős unit distance and pinned distance problems are two problems on distances in finite planar point sets, both introduced by Erdős. Write u(n) for the largest number of pairs at distance one among n points of the Euclidean plane. Spencer, Szemerédi and Trotter proved u(n) = O(n4/3) in 1984, and whether the exponent 4/3 can be lowered was open. The weak pinned distance conjecture asks whether every large n-point planar set has a point from which at least n1−ε distinct distances occur. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim a fixed power saving below 4/3 for u(n) and the weak pinned conjecture. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Erdős introduced the repeated-distance and distinct-distance problems in 1946. His lattice construction gives u(n) ≥ n1 + c/log log n. Spencer, Szemerédi and Trotter proved the upper bound O(n4/3) in 1984, and Székely gave a crossing-number proof. Later work improved the leading constant (Ágoston and Pálvölgyi) and described configurations near the extremal incidence scale (Katz and Silier). Pach, Raz and Solymosi obtained a logarithmic improvement conditional on a rigidity conjecture (SoCG 2026).
- Erdős conjectured u(n) = n1+o(1). An OpenAI construction published on 20 May 2026 (Planar point sets with many unit distances) disproved it, giving at least n1+ε unit distances for a fixed ε > 0 along an unbounded sequence of sizes. Alon and coauthors gave a simplified account (arXiv:2605.20695), and Sawin sharpened the construction to n1.014114 (arXiv:2605.20579). These are lower bounds. The upper exponent remained 4/3.
- For the global distinct-distance problem, Guth and Katz proved that every n-point planar set determines at least a constant multiple of n/log n distances. The pinned question asks for many distances from a single point. Erdős stated it in 1957. Solymosi and Tóth proved a pinned bound of order n6/7, Tardos improved the exponent with entropy inequalities, and Katz and Tardos reached every exponent below (48 − 14e)/(55 − 16e) = 0.864137…. The square grid shows that order n/√(log n) would be best possible. The terminology weak pinned conjecture for the n1−ε form appears, for example, as Conjecture 4.7 of Dewar, Frankl, Mansfield, Nixon, Passant and Warren (arXiv:2505.06590).
The original results
- A power saving for planar unit distances (23 September 2026). Theorem 1.1 of the manuscript states that there are absolute constants 0 < C < ∞ and 1 ≤ β < 4/3 such that u(n) ≤ Cnβ for every n. The manuscript states that it establishes the existence of a fixed positive gap without estimating its size.
- Method, as described: the proof argues by contradiction along a sequence of configurations with nearly n4/3 unit distances. Random cuttings isolate a piece of the point–circle incidence graph with controlled degrees. An entropy estimate feeds a prediction lemma, in the tradition of the entropy methods of Tardos and of Katz and Tardos. After specialization to a number field, the product formula for absolute values converts relations between unit-edge jumps, written in the coordinates x + iy and x − iy, into height bounds. The last step is an algebraic obstruction that uses valuations to change the signs of square roots independently.
- Source: the manuscript A power saving for planar unit distances.
- The weak pinned planar distance theorem (23 September 2026). Theorem 1.1 of the manuscript states that, for each fixed s > 0, the largest possible fraction of ordered pairs (x, y) of distinct points whose distance from x occurs at least ns times among the distances from x tends to zero as n → ∞, uniformly over all n-point planar sets. Its corollary states that, for every fixed ε > 0, all but o(n) points of any n-point planar set determine at least n1−ε distinct nonzero distances, so that every sufficiently large set has such a point. No rate of decay is given.
- Method, as described: real-closed-field transfer puts each configuration in a number field. Squared distance factors in the coordinates x + iy and x − iy, and the product formula is turned into an additive identity for nested partitions built from randomly shifted square grids at the complex embeddings.
- Source: the manuscript The weak pinned planar distance theorem.
- Formalization, as described by the repository. The scope note lean/docs/167.md describes a formal proof of the pinned theorem in its pair-fraction form and of the unit-distance bound with absolute constants C > 0 and 1 ≤ β < 4/3 valid for every n. Its Comparator statements are PinnedDistances.lean and PlanarUnitDistances.lean.
- Catalogue status. Google DeepMind's Formal Conjectures project records Erdős Problem 90 (the unit distance conjecture) as disproved by the May construction, and lists the weak form of Erdős Problem 604 (the pinned distance problem) as research open in FormalConjectures/ErdosProblems/604.lean (checked 18 October 2026, at commit
197f7f8).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 18 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub, review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates the family "full" and records sandboxed Comparator passes for PinnedDistances and PlanarUnitDistances (8 October 2026). Its note says that the Lean pinned statement is the pair-fraction form, from which the pin count follows by a routine pigeonhole step not itself stated in Lean, and that the first paragraph of the scope note calls the unit-distance theorem "not included" although the Lean states it. |
MathVet states that its ratings concern whether the Lean states the headline claims. |
| 2026-10-09 | rohanarun/unit-distance-grid-refinement (GitHub) | Extension of one step (conditional) | A draft that reduces the generic grid used in the final algebraic step of the unit-distance argument from 20 × 5 to 8 × 4, that is from 100 selected edges to 32, with symbolic checks. The README states that this does not improve the unit-distance exponent or give an explicit power saving, and that the manuscript's other steps remain dependencies. | Described by its README as an independent AI-generated research draft prepared with Codex and Claude, without independent mathematical review or formal verification. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists neither PinnedDistances nor PlanarUnitDistances, so both challenges were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-14 (opened), 2026-10-16 (last update) | Formal Conjectures pull request #7340 by bengoechea, with the Lean package MendozaLab/erdos-experiments, proofs/erdos604 | Application (Lean) | Links a Lean counting adapter from the formal pinned theorem of the collection to the weak statement of Erdős Problem 604, that for every ε > 0 the pinned distance count is at least n1−ε for all large n, and attributes the result to the OpenAI manuscript. The pull request states that all 58 modules of the external package compile, that the selected axiom reports use only standard axioms, and that the logarithmic and average variants remain open. It states that Codex was used under the author's direction. | Open pull request, not merged. |
| 2026-10-16 | J. Jardine, Lattice24, referee review of the unit-distance manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | The referee review reports no gap after reading all eight sections and rederiving the main steps by hand. Its one minor note concerns symbols reused with different meanings, which it calls a readability point rather than a mathematical gap. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-18 (merged) | Optimization Constants in Mathematics (GitHub, teorth/optimizationproblems), a crowdsourced repository of best known bounds for optimization constants introduced by Terence Tao in January 2026, entry for the Erdős unit distance exponent |
Catalogue | The entry lists the unit-distance manuscript as the current upper bound 4/3 − ε for an absolute ε > 0, "which is not made explicit", below the Spencer–Szemerédi–Trotter exponent 4/3. Its largest listed lower bound is the exponent 1.04317 from a construction of Naslund (October 2026). | Catalogue entry, proposed in pull request 204 and merged on 18 October 2026 (checked at repository commit 46dbf03). The repository states that submissions are reviewed for plausibility and replicability but are not certified for correctness.
|
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.