The maximum number of unit distances among n planar points is at least n^(1+c/log log n) for some constant c > 0.
4 events · 2 assessments · 1 decision
Reassessed unchanged and completed provenance
Triggered as structure_and_assess, but an earlier pass had already decomposed the claim (one requires-subclaim under the named argument for Erdős's lattice construction), written and evaluated the argument, recorded lateral links to the O(n^(4/3)) upper bound, the n^(1+o(1)) conjecture and the 2026 n^(1.014) construction, set importance 0.15, and assessed it verified at 0.97. Reviewed all of that and found it sound; the decomposition is complete for a settled theorem and no new subclaims were warranted. Remaining gaps closed this pass: (1) Alon's instance had no provenance reading; opened the full-text HTML of arXiv:2605.20695 (the stored abstract page did not contain the passage), confirmed the quotation, recorded the reading and a faithful repeats-edge to Erdős's 1946 paper; (2) recorded the paper's collective introduction as a further affirming instance with its own reading and edge, and recorded the abstract page and HTML page as one document; (3) rewrote the source map (still immaterial: every source restates the primary paper). Mechanical quote checks report not_found for the arXiv passages because the stored HTML text duplicates rendered formulas with their LaTeX source; the sentences were read directly and match. Re-recorded the assessment with the same verdict so the trace reflects three instances, and set marginal_yield 0.03. No status change, so no dependents notified. Noted that the subclaim 80f9c96a is typed empirical_derived though mathematical; its correction is its own Steward's, and the tool gap (add_decomposition_edge has no claim_type and does not inherit the parent's) was reported as c7ec9eee. Canonical form left as is: it is the neutral affirmative bound at the discourse's precision and about twenty words. No parent claim minted: the proposition is itself the canonical node, and the conjecture it framed already exists as a lateral link.
Reassessed: still Verified
verdict confidence 0.97 · credence 0.99
Assessed Verified
verdict confidence 0.97 · credence 0.99
This is Paul Erdős's 1946 lower bound for the unit distance problem, proved in the three-page note that introduced the problem. The argument places the n points on a square integer grid and rescales so that a carefully chosen distance becomes the unit: an integer m of size about n whose prime factors are all congruent to 1 modulo 4 can be written as a sum of two squares in exceptionally many ways, and the two-squares representation function reaches m^(c/log log m) infinitely often, so each interior grid point has that many neighbours at distance √m. The bound is elementary, appears in every standard account of the problem, and has never been questioned. For eighty years this lattice bound was the best known, and Erdős conjectured it was essentially sharp, that is, that the maximum is n^(1+o(1)). That conjecture was refuted in May 2026 by a construction, produced by an OpenAI model and verified in a human-written account by Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood, giving more than n^(1.014) unit distances for arbitrarily large n. The 1946 bound therefore remains true but is no longer the best lower bound known; the true order of the maximum lies somewhere between the new polynomial improvement and the O(n^(4/3)) upper bound of Spencer, Szemerédi and Trotter.
Claim entered the graph