---

Claim. The second question of Problem 1082 has a negative answer. The formal-conjectures file linked above, at the commit of 25 February 2026 that added the proof, proves the theorem erdos_1082b: the statement that every nonempty finite set $A\subset\mathbb{R}^2$ with no three points on a line contains a point from which at least $\lfloor |A|/2\rfloor$ distinct distances to the other points are seen is false. The proof exhibits eight points with coordinates in $\mathbb{Z}[\sqrt3]$, the four points $(\pm2,0)$, $(0,\pm2)$ and the four points $(\pm(1+\sqrt3),\pm(1+\sqrt3))$, checks by computation in $\mathbb{Z}[\sqrt3]$ that no three are collinear, and shows that each sees only three distinct distances. The configuration is Harborth's $H_8$: the vertices of a square and the apexes of the equilateral triangles on its sides, published by Erdős and Fishburn in 1997 and recorded on [[problems/distance_problems/E1082/claims/1997_10_01_erdos_fishburn|its own claim page]] as the accepted answer to this part. A poster identified the two on the site's thread on 25 February 2026, and the site's remarks say the construction was later found by DeepMind.

Covers. The second question, for $n=8$: the same instance as the Erdős–Fishburn page. Nothing is claimed about the first question: the posting says that its proof falsifies the second part of the conjecture, and a reply on the thread notes that the main conjecture remains open.

Depends on. No page of this wiki.

Claimant. The claim was posted on the site's thread on 25 February 2026 by a DeepMind team member under the account GTsoukalas, who reports that a DeepMind prover agent found the Lean proof on 14 February 2026, fully autonomously, the only problem-specific human input being the formal statement from formal-conjectures (pull request 2397), and that the proof compiles with Lean 4.22; the system is not described further on the thread. The proof was merged into Google DeepMind's formal-conjectures repository, which marks the question research solved and points to this proof. The claimant is the organization, with the system named as the thread gives it.

Acceptance. None documented. This corpus has not built or audited the proof, so it gives no formalized evidence; no outside reviewer is recorded; and the site's label for the problem is FALSIFIABLE, so the curator's remark is not an acceptance. The claim is claimed. Its mathematical content is the accepted Erdős–Fishburn claim, which already settles the part.