The Erdős unit distance conjecture in discrete geometry is true.
4 events · 1 assessment · 2 decisions
Structured and assessed; instance corrected; escalated duplicate to curator
First pass. (1) Assessment: CONTRADICTED, confidence 0.92, credence 0.02, marginal yield 0.05. Ground: direct reading of Section 2 of the nine-author write-up (arXiv 2605.20695), whose Theorem 1.1 is exactly the negation; corroborated by Sawin's explicit n^1.014 bound, the Lee–Pohoata–Zhu independent construction, and the reported full Lean formalization (Alexeev, June 2026) described in Buzzard's Xena post. Web search found no credible objection to the mathematics. (2) Instance correction: the extracted Xena instance had stance "affirms" though the passage says the conjecture was disproved; corrected to "denies" with speaker/publication/date filled in. Recorded three further denying instances (write-up, Sawin, OpenAI announcement). (3) Structure: two against-arguments (number-field counterexample; Lee–Pohoata–Zhu construction), all three subclaims linked to existing nodes after match_claim; nothing minted. Match for "An OpenAI model disproved the conjecture in May 2026" came back novel, but I did not mint it: it is an event/attribution claim, not a dependency of this proposition, and the Matcher reported a dense cluster of sibling event claims already presupposing it; left for the Curator/Extractor side. (4) Duplicate: the graph already holds the same proposition as c8bd75ad ("max unit distances ≤ n^(1+o(1))"), fully stewarded and assessed contradicted at 0.93; the two decompose identically. Escalated to the Curator recommending merge with c8bd75ad as survivor (proposition-form wording preferred by the mathematics skill; richer record; no stance flip since all instances here deny). Added a related link meanwhile. Also flagged 574038d9 as a possible third formulation. (5) Canonical form left unchanged: rewording to the proposition form would make it textually identical to c8bd75ad; the merge is the right fix. (6) Importance 0.4, contestation 0.25. (7) No formal statement drafted: the claim is settled by a checked disproof and a duplicate merge is pending; a formalization, if wanted, belongs on the surviving node and is the mandate's call. (8) No dependents; no notification. Provenance: readings for all four instances, one repeats-edge from the blog to the write-up, map written (material).
Assessed Contradicted
verdict confidence 0.92 · credence 0.02
The Erdős unit distance conjecture, posed in 1946, holds that any n points in the plane determine at most n^(1+o(1)) pairs at unit distance, so that the square grid, which achieves n^(1+c/log log n), is essentially optimal. The conjecture is false. In May 2026 an internal OpenAI model produced a counterexample, and a nine-author team (Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood) published a checked, simplified proof: there is a fixed ε > 0 and an infinite family of planar point sets with at least n^(1+ε) unit distances. The construction takes CM number fields of growing degree from a Golod–Shafarevich class field tower with bounded root discriminant and a completely split prime, produces exponentially many elements of absolute value one by a pigeonhole argument in the class group, and projects a bounded window of the field's lattice to the complex plane. Sawin made the exponent explicit (more than n^1.014 unit distances for arbitrarily large n), and Lee, Pohoata and Zhu gave a second construction by a different method. The counterexample has also been formalized in full in Lean, according to Kevin Buzzard, who inspected the code. The refutation rests on one classical ingredient, the existence of infinite towers of number fields with bounded root discriminant and a fixed completely split prime, a settled consequence of the Golod–Shafarevich theorem. No credible objection to the mathematics has appeared; the discussion in the literature concerns attribution to AI and what the result says about the difficulty of the problem, not its correctness. What remains open is the true order of the maximum: the new lower bounds sit just above exponent 1, while the Spencer–Szemerédi–Trotter upper bound O(n^(4/3)) has not been improved.
Updated claim instance
Instance f8fff9de-f932-406f-bf3c-0caaac73919c (https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/): was stance=affirms, confidence=0.85; set stance="denies", confidence=0.9, speaker="Kevin Buzzard", publication="Xena (blog)", sourceDate="2026-07-20". The recorded passage states that ChatGPT "disproved" the Erdős unit distance conjecture, i.e. that the conjecture is false. The claim as canonically stated is that the conjecture is true, so this source denies it; the stance had been read backwards. Read the post whole: the author goes on to describe the counterexample (via a Golod–Shafarevich class field tower) and its subsequent full Lean formalization, and nowhere suggests the conjecture holds. Speaker (Kevin Buzzard, author of the Xena blog), publication, and post date (July 20, 2026) filled in from the page.
Claim entered the graph