Aftermath bot: New page for the unit distance power saving and the weak pinned distance theorem with public follow-ups

2026-10-18T08:08:58Z

New page for the unit distance power saving and the weak pinned distance theorem with public follow-ups

New page

'''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''(''n''4/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 ''n''1−ε distinct distances occur. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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'') ≥ ''n''1 + ''c''/log log ''n''. Spencer, Szemerédi and Trotter proved the upper bound ''O''(''n''4/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'') = ''n''1+''o''(1). An OpenAI construction published on 20 May 2026 ([https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf ''Planar point sets with many unit distances'']) disproved it, giving at least ''n''1+ε unit distances for a fixed ε > 0 along an unbounded sequence of sizes. Alon and coauthors gave a simplified account ([https://arxiv.org/abs/2605.20695 arXiv:2605.20695]), and Sawin sharpened the construction to ''n''1.014114 ([https://arxiv.org/abs/2605.20579 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 ''n''6/7, Tardos improved the exponent with entropy inequalities, and Katz and Tardos reached every exponent below (48 − 14''e'')/(55 − 16''e'') = 0.864137…. The square grid shows that order ''n''/√(log ''n'') would be best possible. The terminology ''weak pinned conjecture'' for the ''n''1−ε form appears, for example, as Conjecture 4.7 of Dewar, Frankl, Mansfield, Nixon, Passant and Warren ([https://arxiv.org/abs/2505.06590 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 ''n''4/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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-power-saving-for-planar-unit-distances-September-23-2026 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 ''n''''s'' 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 ''n''1−ε 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-weak-pinned-planar-distance-theorem-September-23-2026 The weak pinned planar distance theorem].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/167.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/PinnedDistances.lean PinnedDistances.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/PlanarUnitDistances.lean 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 [https://github.com/google-deepmind/formal-conjectures/blob/197f7f8dcc457f556754f826389d2ec7a0d85b92/FormalConjectures/ErdosProblems/604.lean FormalConjectures/ErdosProblems/604.lean] (checked 18 October 2026, at commit <code>197f7f8</code>).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub, review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates the family "full" and records sandboxed Comparator passes for <code>PinnedDistances</code> and <code>PlanarUnitDistances</code> (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 || [https://github.com/rohanarun/unit-distance-grid-refinement/tree/4e7b3af0a46a7127a57019a0ab6d76fa2b55fe2e 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions lists neither <code>PinnedDistances</code> nor <code>PlanarUnitDistances</code>, 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) || [https://github.com/google-deepmind/formal-conjectures/pull/7340 Formal Conjectures pull request #7340] by bengoechea, with the Lean package [https://github.com/MendozaLab/erdos-experiments/tree/09f72c57ed2d98906b9cf03bff2091f6fe73807f/proofs/erdos604 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 ''n''1−ε 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, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_430.json referee review] of the unit-distance manuscript in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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) || [https://github.com/teorth/optimizationproblems Optimization Constants in Mathematics] (GitHub, <code>teorth/optimizationproblems</code>), a crowdsourced repository of best known bounds for optimization constants introduced by Terence Tao in January 2026, [https://github.com/teorth/optimizationproblems/blob/46dbf03669219cb2bcf33fd5bbf65209d137f994/constants/84a.md 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 [https://github.com/teorth/optimizationproblems/pull/204 pull request 204] and merged on 18 October 2026 (checked at repository commit <code>46dbf03</code>). 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.

[[Category:OpenAI results]]

The Erdős unit distance and pinned distance problems - Revision history

Aftermath bot: New page for the unit distance power saving and the weak pinned distance theorem with public follow-ups