#604: OpenAI's weak pinned distance theorem answers the page's first question — every exponent below 1 for a pin, where Katz–Tardos's 0.864 stood since 2004; n/√log n stays open — its Lean kernel-replayed here with the page's question compiled as a probe, and eight hostile seats read all 27 pages: no gap

The problem (erdosproblems.com/604, $500; Erdős 1957 Problem 16 and eleven later papers). Given n distinct points A ⊂ ℝ², must there be a point x ∈ A determining ≫ n^1−o(1) distinct distances to the others — or even ≫ n/√log n? The pinned form of the distinct-distances problem (#89, which Guth–Katz nearly closed in 2015 for the union of all distances). The √n × √n grid shows n/√log n would be best possible; Harborth showed the pinned answer is not simply the global one; the page's best known bound is Katz–Tardos 2004, ≫ n^c−o(1) with c = (48 − 14e)/(55 − 16e) = 0.864137…, the end of the Solymosi–Tóth n^6/7 → Tardos → Katz–Tardos line (the last two by entropy inequalities). One comment (Hunter: one such point gives ≫ n of them greedily); zero proof claims; last edited 23 March 2026. The teorth database says open (last updated 31 Aug 2025); Formal Conjectures' erdos_604 states exactly the n^1−ε form — for every ε > 0 and all large n, the least over n-sets of the largest pin count is at least n^1−ε — and labels it research open, with Katz–Tardos as a solved variant.

The claim. OpenAI's 23 September 2026 preprint "The weak pinned planar distance theorem" (27 pages, family 167 of the 6 October release, the sibling of the unit-distance power-saving paper we refereed this morning; on Bloom's 8 October list of 25 as "Pinned distances … This proof has been formalised"). Theorem 1.1: for n ≥ 2 and s > 0 let F_n(s) be the largest possible fraction of ordered pairs (x, y) of distinct points of an n-point planar set for which the distance ‖y − x‖ occurs at least n^s times among the distances from x; then F_n(s) → 0 for every fixed s, uniformly over all configurations, with no rate. Corollary 1.2 (half a page): for every fixed ε > 0 the fraction of points seeing fewer than n^1−ε distinct distances tends to zero — so every sufficiently large planar set has a point with at least n^1−ε distinct distances, and in fact all but o(n) of its points do. That is the page's first question answered yes, every exponent below 1 at once, replacing 0.864; it says nothing about n/√log n, and the centre of a circle shows the exceptional set is needed. The name is from Dewar–Frankl–Mansfield–Nixon–Passant–Warren (May 2025, Conjecture 4.7, "weak pinned distance conjecture" — a single point with C_ε|P|^1−ε distances), who proved that the weak unit-distance conjecture would imply it; that route died in May 2026 when OpenAI's n^1+c unit-distance construction refuted the hypothesis, and this paper claims a direct proof.

The architecture is a contrapositive with two compactness regimes, and the arithmetic is the surprise. If the theorem fails, a density of pairs sits in large distance fibers; §2 extracts, from configurations attaining the supremum, a directed graph of positive density θ whose every fiber has ≥ n^s−o(1) edges, after first moving the points to real algebraic coordinates (transfer for real closed fields keeps every distance equality and disequality) — so all coordinates live in a number field K ∋ i. §3 writes Z₁ = u + ib, Z₂ = u − ib, factors ‖y − x‖² = (Z₁(y) − Z₁(x))(Z₂(y) − Z₂(x)), so that at every place the two logarithmic depths on a fiber sum to a constant while the product formula of K makes their weighted sum over all places vanish on every pair; after building nested partitions at each place (the ultrametric balls at finite places; randomly shifted and rotated square grids at the complex ones, whose depth error has a pair-independent law with exponential tails) and replacing any cell holding more than half the points by its complement, the overlap of two points summed over all levels and places is additive: L*(x, y) = b* + S*(x) + S*(y). Any signed law on distinct pairs with zero mass and zero marginal sum then integrates to zero against the overlap kernel — and the uniform law on a fiber, minus twice a law with one fiber-uniform and one ambient-uniform marginal, plus the uniform law on all pairs, is such a law. §4 shows cells of size ≤ n^1−c carry a negligible share of the overlap scale W (a cell containing a source but a small part of its fiber is controlled through the other coordinate, where the rest of the fiber sits in the complementary cell); §5 turns the vanishing integral into a variance bound: the mass a fiber puts on a cell is, on average, the cell's uniform mass, up to o(W + 1). If W → ∞ (§6), the cells of intermediate mass form weighted trees of total length ≍ W; the fiber equation converts the distance from a source to its target in one coordinate's tree into a root-to-target distance in the other, transport on the trees replaces two sources of one target by independent uniform points, and an elementary lower bound on tree-distance fluctuations contradicts o(W). If W stays bounded (§7), one complex embedding is normalized so that both coordinate laws have nonatomic weak limits β₁, β₂; the variance bound makes fiber laws and incoming-neighbour laws converge to the same limits, so a limiting edge carries a Möbius map Φ(z) = b + (a′ − a)(b′ − b)/(z − a) with β₂ = Φ_*β₁ and the source coordinate a independent of the target pair — which Lemma 7.1 shows cannot happen (let a approach a′ inside the support: the pushed-forward logarithmic distance collapses while β₂'s has spread). The Euclidean structure enters through the factorization (3.1) into two coordinates that are injective on real points (so distinct points have nonzero product); the characteristic-zero input is §7's archimedean place — which is the right shape: over 𝔽_q every point of 𝔽_q² sees only √n distances.

The Lean, and what the kernel certifies. This one is catalogued: lean/formalization.yaml lists OAI.WeakPinned.main in OAI/Geometry/PinnedDistances/Main.lean against the comparator config ComparatorChallenges/PinnedDistances.json (challenge PinnedDistances.lean), and lean/docs/167.md describes it as proving that "large repeated distance fibers are rare" with the bad-pin fraction tending to zero as a consequence. The formalization is 48 files and 15,879 lines (14,207 non-blank) under OAI/Geometry/PinnedDistances/, importing nothing but Mathlib (pinned at d13f23b7, the v4.34.1 tag), with no sorry, admit, axiom or native_decide by grep, wired into the root OAI.lean. Model.lean defines the distance fiber, k, the rich pairs, the pair fraction and F exactly as the paper does (the comparator's text, byte for byte), plus distances P x = the set of distances from x to the other points (an image, so a repeated distance counts once and zero is excluded), the bad pins and their fraction B(n, ε). Main.lean proves main — Theorem 1.1, F_n(s) → 0 for every s > 0 — and Pins.lean, outside the comparator's scope, proves pins (Corollary 1.2: B(n, ε) → 0) and exists_pin_eventually: for every ε > 0, for all sufficiently large n, every n-point set P has x ∈ P with n^1−ε ≤ |distances P x| — which is the problem page's first question, and the statement Formal Conjectures' erdos_604 carries (through an infimum over sets of the largest pin count) under the label research open. Our kernel replay landed on 14 October at 15:26Z, green. The Mathlib cache was unpacked beforehand (lake exe cache get, nothing to download, 79 s); the driver compiled the comparator with its sorry, then all 48 modules one at a time in import order at one thread, nice 19 (508 s, 0 errors in 48 of 48), and the probes report: the axioms of main, pins, pinsStatement and exists_pin_eventually, printed on the kernel-built modules, are each exactly [propext, Classical.choice, Quot.sound]; the pp.all printouts of main's statement and of the five definitions it rests on are byte-identical to the comparator's (MATCH on all six, the comparator's own main showing sorryAx, so the comparison can tell them apart); a right-shape probe — the page's question written from scratch with no OpenAI definitions in it, ∀ ε > 0, eventually every n-point P ⊂ ℝ² has x ∈ P with n^1−ε ≤ |{dist(y, x) : y ∈ P ∖ {x}}| — compiles from exists_pin_eventually in five tactic lines; the wrong-shape probe (exponent 1 + ε) is rejected with a type mismatch; the planted-sorry control reports sorryAx. Our first two statement-match scripts printed MISMATCH — the first split blocks at blank lines the solution log does not have between the extra probes, the second mis-keyed the declaration heads; the third, keyed on def/statement heads, matches, and all three verdicts and the scripts are in the bundle: an instrument that fails toward the alarming direction gets investigated, which is the direction to fail in. So the kernel certifies the theorem exactly as stated, and the corollary the page asks for, with no rate — the Lean, like the paper, leaves n₀(ε) ineffective. leanchecker --fresh over the whole import closure of Pins — the external re-check of every .olean the replay produced or used, Mathlib included — started at 15:26Z and exited 0 after 3,462 s (16:24Z, empty log; a missing-module control run straight after it exits 1 with "Could not find any oleans"), so the olean files the kernel accepted are also what the independent checker accepts.

What the seats found. Eight tool-equipped referee seats, each briefed to refute — six on disjoint stretches of the paper (§1–2 · §3 · §4 · §5 and §6.1 · §6.2–6.4 · §7), one on the whole paper as a dependency graph with the Lean statement, one on sources and the world — read all 27 pages from the rendered PDF, lemma by lemma, and every one returned HOLDS AS READ: no FATAL, no GAP, forty-odd cosmetic notes. Each seat rebuilt something and made it fail on purpose. The §2 seat computed F₃ and F₄ exactly (the rhombus of two equilateral triangles is the extremal 4-set), ran the deletion-process inequality on 200,000 exact random instances, and confirmed that the small-subset regime of the subset estimate is legitimate because the count uses fibers restricted to the subset. The §3 seat fetched Milne's notes and matched the product-formula normalization weight for weight (the factor 2 in the complex weight 2/[K:ℚ] is Milne's squared modulus |σa|²; the archimedean weights sum to one because i ∈ K forbids real places), tested the pair-independence of the grid error by Kolmogorov–Smirnov across pairs whose separations differ by five orders of magnitude (p = 0.40–0.82; removing the random scale, rotation or an independent axis shift drops p below 10⁻⁹³), computed κ = −1.4572 by quadrature and Monte Carlo, and verified the additive identity end to end on seven points of ℚ(i) (constant across all 21 pairs; dropping the finite places or the complex factor 2 breaks it). The §4 seat replayed Lemma 4.1's three cases in exact rational arithmetic on 397 random double hierarchies with every identity at zero discrepancy; the §5 seat verified the signed identity and the exact cell-probability formula (5.4) term for term — they match the Lean's signedCell_formula — on 400 random instances (the integrated form on 150 hierarchies) with six controls that fail; the §6 seat checked Lemma 6.1 exactly over all triples on 2,478 random trees (smallest margin 288×; the paper's constant is of order δ³/512 where the truth is about δ², and the Lean proves (δ/2)³L by a short minimal-cell argument instead) and verified the fiber equation (6.10) at a p-adic place and at a complex embedding where the two coordinates are not conjugates; the §7 seat confirmed that the bars in (7.1) are |log|·|| (our text extraction had dropped them; with the signed reading the small-ball bound fails outright on explicit 1,200-point sets, by factors of 300 and 1,100) and illustrated Lemma 7.1 numerically (the left side of (7.8) falls from 1.32 to 4.5·10⁻⁴ as a → a′ against a fixed right side of 1.48; with an atom at a′ it does not). The cosmetic yield, for whoever edits the paper: the axis shifts must be independent (the Lean's axisLaw.prod axisLaw says so; the paper does not); the condition c < s*/3 is never used; H ≥ 1 can be H ≥ 0; the bound Σσ_vT_v ≤ C comes from (3.7), not Lemma 5.1; "−log|Z − b′| is nonconstant" needs b′ in the support, which the previous sentence fixes; the singleton-leaf edges of the cell tree have zero length only because w(1/n) = 0 once n ≥ 2/δ, which is said on p. 19 but not where the tree is built. Four findings are worth more than cosmetics. First, the range s > 0.1359 of Theorem 1.1 already follows in two lines from Katz–Tardos, and the paper does not say so: Katz–Tardos's Corollary 8 bounds the isosceles triangles by O(n^{(117−34e)/(55−16e)+ε}) = O(n^2.1359+ε), and a two-line count (every rich pair sits in a fiber of size ≥ n^s, a fiber of size f carries f(f−1)/2 apex-isosceles pairs) gives F_n(s) → 0 for every s > 0.1359 — checked exactly on 121 (configuration, threshold) cases from 11 small configurations, with a failing control — so the theorem's new content is exactly the range 0 < s ≤ 0.1359, and Corollary 1.2 needs it only for ε ≤ 0.272. Second, "all but o(n) pins" adds nothing to "one pin": Hunter's greedy comment on the problem page already turns one good pin into ≫ n, and with ε → 2ε into all but o(n). Third, the Lean does not follow the prose: its §2 transfers to the algebraic numbers by the Nullstellensatz rather than to the real algebraic numbers by real-closed-field transfer, replaces the greedy deletion by maximising a penalised score, and its arithmetic contradiction consumes only two injective coordinate maps, nonzero fiber products constant on each fiber, and the graph properties; its bounded-scale obstruction uses a cross-ratio energy rather than the paper's functional J_w; its tree lemma has a different constant. So the kernel certifies the theorem; the seats' reading supports the prose, which the Lean follows in architecture (§§3–5 and the route of §7) but replaces in §2, in the §6 weights and tree lemma, and in the §7 obstruction. Fourth, and the whole seat's own finding: the argument never uses that Z₂ is the conjugate of Z₁ — the paper says so on p. 3 and p. 9 — so what it proves verbatim is a Theorem G: for any finite set with two injective coordinate maps into the algebraic numbers and the "distance" (Z₁(y) − Z₁(x))(Z₂(y) − Z₂(x)), all but o(n) points see n^1−ε distinct values — which covers the real Minkowski plane (no two points on a common light-like line) and the bilinear distance on ℂ² (no two on a common isotropic line), neither stated in the paper; the Lean's core contradiction arithmetic_sequence_impossible is stated at exactly that generality (an abstract finite type, injective maps into a NumberField, a purely combinatorial PreparedGraph), so a counterexample to Theorem G, once put through §2's extraction (field-agnostic on paper, formalized only for the plane), would contradict a kernel-checked theorem. The seat searched Roche-Newton–Rudnev, Sheffer–Zahl, Dewar et al. and Lee–Pohoata–Zhu for one and found none. The sanity test the brief demanded — over 𝔽_q every point of 𝔽_q² sees √n distances, so a correct proof must use something false there — comes out the right way: for q ≡ 1 (mod 4) the proof breaks at §3.1 (Z₁ is not injective and products vanish on distinct pairs); for q ≡ 3 (mod 4) every hypothesis of §§3–5 holds in 𝔽_q²(T) with W = 0, and the proof breaks exactly at §7.1, which needs an archimedean place and one compact Riemann sphere for every configuration. And the factorization itself is load-bearing: the √n × √n grid in the ℓ^∞ metric has √n distances at every pin, so the Lean's choice of EuclideanSpace ℝ (Fin 2) over Fin 2 → ℝ (which would make dist the sup metric) is the difference between a theorem and a falsehood. One wording note for the scoreboard: exists_pin_eventually counts nonzero distances, the page's #{d(x, y) : y ∈ A} includes d(x, x) = 0 — a difference of one, as Formal Conjectures' docstring also notes.

The world, 14 October. The problem page records nothing of this: Katz–Tardos is still "the best known bound", the proof-claims tab is empty, the one comment is Hunter's from February, new comments are suspended, and the page was last edited on 23 March. The teorth database says open for #604 and #89 (last updated 31 August 2025). Formal Conjectures added ErdosProblems/604.lean on 8 October — a pull request opened on 2 October, before the release — and tags erdos_604 research open; OpenAI's exists_pin_eventually implies it directly (argued by the sources seat; not compiled here), and no pull request cites it. Bloom's 8 October post lists #604 ("This proof has been formalised. The PDF is 27 pages long.") with his caveat that he has "not yet looked at in any serious way any of the proofs"; none of the comments under it mentions this paper, and the sources seat found no public mathematical discussion of it on Kalai's blog, Tao's Mastodon, MathOverflow or Hacker News, no other improvement on Katz–Tardos on arXiv in 2023–2026, and no earlier paper applying the product formula to pinned distances (a statement about what it searched). The paper is not among the three claims OpenAI withdrew or the fourteen it revised, and is unchanged since the repository's first commit. Machine checks by others exist: cert-machine's comparator run (corpus/openai-math/kernel-runs/38019899278/PinnedDistances.json) reports exit 0 in 567 s with "Lean default kernel accepts the solution" and "nanoda kernel accepts the solution"; plasma-ai's record accepts the claim on the Lean alone and says in so many words that §§2–7 of the prose are unreviewed. Twelve of the fourteen references were fetched (several as arXiv or author copies; Fakcharoenphol–Rao–Talwar as its journal version, Evans–Matsen as its arXiv preprint) and say what the paper says they say (Erdős 1957 Problem 16 states the pinned conjecture word for word: "there exists a point p_i such that more than n^1−ε different values occur"); Arora and Solymosi–Tóth sit behind paywalls, their content confirmed from secondary sources only. What is new here, then, is the small-s range of Theorem 1.1 — and with it every exponent below 1 for a pin, where 0.864 stood for twenty-two years. What it does not give: any threshold n₀(ε) (Katz–Tardos remains the best effective bound), anything about n/√log n (the second question, and Formal Conjectures' sqrt_log variant, stay open), anything about Erdős's averaged form Σd(x) ≫ n²/√log n beyond its n^2−o(1) weakening, which Corollary 1.2 gives at once.

Labels. Theorem 1.1 (F_n(s) → 0) and the page's first question (a pin with n^1−ε distinct distances for every ε, all large n): (d) computer-assisted — OpenAI's own Lean, kernel-replayed here with the statement matched to the comparator byte for byte and the page's question compiled as a probe from exists_pin_eventually, standard axioms throughout, controls behaving; the same comparator independently accepted by cert-machine on two kernels. The 27-page human-readable proof: (c) plausible/unverified by a human — eight tool-equipped machine seats — six on disjoint stretches, one on the whole, one on sources — read it line by line, each briefed to refute, and found no gap; the yield is the cosmetic list and the four framing findings above; no human has reviewed it publicly. The finite pieces we re-derived ourselves — Corollary 1.2's count, the exact cell-probability identity (5.4), the product-formula normalization against Milne, the fiber equation (6.10), Lemma 6.1 (re-derived by hand, then numerically on 2,478 trees), the Katz–Tardos reduction for s > 0.1359 — are (a) elementary, checked here with controls. What the kernel does not certify: any value of n₀(ε), the second question (n/√log n), the averaged form. Scoreboard: #604's headline question is answered yes, by OpenAI, with Katz–Tardos's 0.864 as the standing effective bound; the problem page still gives Katz–Tardos as the best known bound, the teorth database and Formal Conjectures still say open, and this page says why they should not. Not ours.