---

Claim. The answer to Problem 90 is no, with an explicit exponent. Theorem 1 of Will Sawin, An explicit lower bound for the unit distance problem, arXiv:2605.20579v1, submitted 20 May 2026, states that for arbitrarily large $n$ there is a set of $n$ points in the plane with at least $n^{1.014114}/C$ ordered pairs at distance one, for an absolute constant $C$; counting unordered pairs changes only the constant. The fixed exponent gain exceeds $C/\log\log n$ for every fixed $C$ once $n$ is large, which refutes the bound the problem asks about. The construction, carded at sawin_2026_explicit_lower_bound_unit_distance_problem, works in a CM-field lattice: the relative norm-class group is bounded through units and relative class numbers, ideals whose norm is a product of powers of small split primes are pigeonholed in it, Louboutin's relative class-number estimate and the cyclotomic discriminant formula control the constants, and the fields come from an unramified pro-$2$ tower with controlled inertia. The paper prints the gain only as the decimal $0.014114\ldots$. The rational interval check certifying $\delta>0.014114$ is the corpus's own work, on the Theorem 1 result page, and awards no standing. The result is stated along a sequence and not for every large cardinality.

Depends on. No page of this wiki. The outside theorems the paper uses are declared inputs on the linked result pages and are not reproved there.

Acceptance. None documented. The paper is the arXiv v1 manuscript; no later version, journal reference or publication was known on 2026-09-06. The site's page labels the problem disproved and credits the disproof to an internal model at OpenAI (its page is OpenAI); it does not credit this paper, so the curator's label is no review of it. The corpus's own reading awards no standing. Emmerich's report, paged at Proposition 2, reproduces the certificate value digit for digit and re-optimizes it to $\delta=0.0152616\ldots$ with Sawin's prime set unchanged, conditional on Sawin's criterion being applied exactly as stated; that reproduces the arithmetic of the certificate and does not review the proof; the re-optimized certificate is claimed on Emmerich's page. The claim is therefore claimed. Sawin is also a coauthor of the companion manuscript on its own page, whose qualitative construction is different.

Formalization. None of this result. Naganori Yamaguchi's repository SawinTotallyRealTowers states a form of the companion manuscript's Proposition 2.3: one infinite set of primes congruent to $1$ modulo $4$ splits completely in totally real fields of unbounded degree with bounded root discriminant. The formal-conjectures statement file for Problem 90 attaches it, from its commit of 7 September 2026, to its sawin_totally_real_tower, and that file's docstring and the repository's README credit the statement to Sawin. Sawin's Lemma 11 and Lemma 12 treat only a finite set of primes, bounded by the tower condition, and give them inertia degree at most $2$. They state no such result. The problem page records the development.