Erdős unit distance exponent

Upper bound, last-listed row

| $4/3 = 1.333\dots$ | [SST1984] | Spencer, Szemerédi and Trotter; via the Szemerédi–Trotter incidence theorem. |tracked since 2026-07-24 — no movement seen yet

Lower bound, last-listed row

| $1.03583\dots$ | [MO511514] | Naslund, revised (≈25 May 2026); replaces the sphere-packing estimate by a covolume bound on the ideal lattice (asserted to be essentially optimal for this part of the argument), re-optimizing to $\lvert T\rvert = 39$. Hybrid ChatGPT 5.5 Pro / human work. Current best. Unverified. |text edited 2026-08-23 — bound unchanged

Checked against material for its cited source

• Another row, not one shown above: bound row $> 1$ (inexplicit) line 25 citing [ABGLSSTWW2026] — the claim we checked: that a parameter choice in [ABGLSSTWW2026] gives epsilon approximately 6.24 times 10^-38 in the row’s construction with u(n) bounded below by a positive constant times n^(1+epsilon) for infinitely many n. The reference [O2026], the model attribution and the stated number-field method are not checked here. What we read supports it: the proof of Theorem 1.1 fixes example parameters and states that the exponent can then be taken to be about 1 + 6.24 × 10^−38, for point sets whose size goes to infinity. source link (read in the arXiv preprint version 1 (20 May 2026), the only version: Theorem 1.1, the parameter choice and equation (2.2) on pp. 1–6, from page images). Selected: drawn by its position in the list of cited rows, not because it looked wrong.
• Another row, not one shown above: bound row $1$ line 24 citing [E1946] — the claim we checked: that Erdős's 1946 paper gives the integer-lattice construction u(n) ≫ n raised to the power 1 + c/log log n, and conjectures it is sharp. What we read supports the construction, and supports 'sharp' only as a conjecture that the exponent 1 is sharp, not that n raised to the power 1 + c/log log n is the exact order. This verdict does not cover the row's own step 'hence limsup … ≥ 1', which was not asked of the source. source link (read in the body: a scan of the printed Monthly article, pp. 248–250, from the Rényi Institute's Erdős archive (users.renyi.hu/~p_erdos/1946-03.pdf), printed p. 249 read from the page image). Selected: drawn by its position in the list of cited rows, not because it looked wrong.

2 bound row(s) here have been checked against material for their cited source (2 drawn by position, 0 chosen because something already looked wrong). Across this whole ledger 70 row(s) have been drawn by position, against 691 rows that name a source, counted on 2026-09-27: 64 were checked against material for their cited sources and for 6 the cited source could not be read at all. 5 more were chosen for suspicion and checked; they are counted apart, because a set selected for suspicion carries no rate. A row not listed here has NOT been checked.

Outside the source table: a claim in OpenAI's math release

• Family 167, “Planar distinct distances and unit-distance bounds”, claims that n points in the plane determine at most C·n^β pairs at distance one, for fixed constants C and β with β < 4/3.

  Its Lean statement, PlanarUnitDistances.lean:

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

  Same quantity: the file's u(n) is the largest number of unit-distance pairs among n points in the plane, as in this constant's definition, so the statement bounds the exponent by β, below the 4/3 in this constant's last-listed upper-bound row. No value of β is given.

  Status: a Lean statement of it is published with a proof by its authors. We read the statement and it matches this constant's definition; we have not compiled the proof, and we have not read the paper.

A claim in a preprint release, read at openai/math@fd4aeeb on 2026-10-12. It is not in the source table, and this ledger has not changed the rows above because of it.