---

Claim. The answer to Problem 90 is no. Let $\nu(n)$ be the largest number of unordered pairs at Euclidean distance one among $n$ distinct points of the plane. The claimed result is Theorem 1.1 of the report Planar Point Sets with Many Unit Distances, authored by OpenAI and attributed by the report to an internal OpenAI model: there is an absolute constant $\delta>0$ and there are infinitely many $n$ with

$$\nu(n)\geq n^{1+\delta}.$$

For every fixed $C>0$ the right side exceeds $n^{1+C/\log\log n}$ once $n$ is large, so the bound $n^{1+O(1/\log\log n)}$ the problem asks about fails along that sequence. The report is carded at openai_2026_planar_point_sets_many_unit_distances and the theorem is paged at Theorem 1.1. The construction takes a totally real cyclic cubic field and an everywhere-unramified pro-$3$ tower over it, kills the Frobenius classes of many fixed rational primes while the Golod--Shafarevich inequality keeps the tower infinite, adjoins $i$, and pigeonholes ideals whose norm is a product of the chosen split primes into one class, so that a lattice of bounded root discriminant carries exponentially many elements of absolute value one; a product-disc window averaged over the lattice and projected injectively to the plane gives the point sets. The report's PDF metadata gives a creation date of 19 May 2026; the site's page crediting the result was last edited on 20 May 2026, the day Sawin's arXiv:2605.20579 and the companion arXiv:2605.20695 were submitted, so the posting is dated 20 May 2026 here.

Depends on. No page of this wiki. The conductor-discriminant formula, the Frattini presentation bound, Shafarevich's relation-rank estimate, the Golod--Shafarevich inequality, Chebotarev's density theorem, the prime number theorem in arithmetic progressions and the Minkowski class-number estimate are outside inputs, declared at statement level on the result pages and not reproved there.

Acceptance. The reviewed evidence is the check of the model's proof documented in the companion manuscript Remarks on the disproof of the unit distance conjecture, arXiv:2605.20695v1, by nine mathematicians, none an author of the report: its abstract presents the manuscript as a "human-verified version" of the OpenAI counterexample, and its Section 6, written by Daniel Litt, records that Litt was asked by OpenAI to check the solution's correctness and became convinced that it is correct. Beside it, the site's curator, Thomas Bloom, labels the problem disproved and credits the disproof to an internal model at OpenAI that constructed, for infinitely many $n$, an $n$-point set with at least $n^{1+c}$ unit-distance pairs for an absolute $c>0$; the curator is not an author of the report but is a coauthor of the companion manuscript, which calls its own proof a human-digested version of the model's and has its own page, Alon and coauthors; Sawin's explicit construction is a third page, Sawin. The report's own account of AI-assisted verification, review by external mathematicians and human editing is the source's attestation. The retained [[../library/discrete_geometry/openai_2026_planar_point_sets_many_unit_distances/evidence/verify/full_review|full review]] of the reconstructed proof, relative to the seven outside inputs named above, is this project's own and counts for nothing here. No journal publication or arXiv version of the report is known. The repository plby/Erdos90, pinned above at its commit of 27 June 2026, says in its README that it holds a formal Lean proof of OpenAI's counterexample, with a submission that the Lean comparator's provenance record describes as Boris Alexeev's formalization, produced by Codex over about a month and verified on lean-eval on 26 June 2026. The repository logical-intelligence/erdos-unit-distance, pinned above at its commit of 28 May 2026, calls itself in its README a Lean 4 formalization of the disproof of the planar unit-distance conjecture by OpenAI, 2026, produced by the company's Aleph Prover agentic system; its main_theorem reaches the fixed-power statement conditionally on two textbook theorems stated as hypotheses in its signature, the Golod--Shafarevich inequality for finite $p$-groups and Shafarevich's relation-rank bound, and the company's page of 28 May 2026 says external reviewers checked the statement translation and the two theorems. The corpus has built and audited neither development, so the page lists no formalized evidence. The problem page's Formalization section records the other Lean developments and what each covers.