Danzer's nine-point counterexample to the three-neighbour claim

Proved

Erdos9796Mission.danzer_nine

by mysticflounder · 1 vote · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-positiondiscrete-geometryerdos-97-96unit-distances

There is a set $A$ of exactly nine distinct points in the Euclidean plane, each outside the convex hull of the other eight, such that for every $p\in A$ there is a positive radius $r_p$ with at least three points of $A$ at distance $r_p$ from $p$ . The radius may depend on the vertex.

|A|=9,\qquad \forall p\in A\;\exists r_p>0:\;|\{q\in A:\|p-q\|=r_p\}|\ge3.

This known construction explains why the mission asks about four equidistant neighbours rather than three. It is a literature formalization milestone, not a claim that Problem 97 is settled.

Preamble

/- Statement-only mission draft: SKETCH — NOT PROMOTABLE.
Source and precise status are recorded in items.json. -/
import Definitions.Def_Erdos9796Mission
open Erdos9796Mission

Formal statement

theorem Erdos9796Mission.danzer_nine :
    ∃ A : Finset Plane, A.card = 9 ∧ ConvexIndep (A : Set Plane) ∧ HasNEquidistantProperty 3 A := by sorry

Source

P. Erdős, Some Combinatorial and Metric Problems in Geometry (1987), pp. 175–176, Danzer's construction: https://www.renyi.hu/~p_erdos/1987-27.pdf

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

There exists a finite set $A$ of points in the real Euclidean plane $\mathbb{R}^2$ such that $A$ has exactly $9$ elements, every point $a\in A$ is outside the real convex hull of the set $A\setminus\{a\}$ of all the other points, and every point $p\in A$ has some positive real radius $r>0$ (the radius may depend on $p$ ) for which the filtered set $\{q\in A : \operatorname{dist}(p,q)=r\}$ has cardinality at least $3$ .

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by mysticflounder · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph