Unit-distance representations of seven-vertex graphs or their complements in R³

For every simple graph G on seven vertices, must either G or its complement admit an injective unit-distance representation in R³? Only edges are required to have length one; nonedges are unrestricted.

Why it matters and what counts as progress

Why it matters: This is the d=3 instance of the broader 2d+1-vertex dimension question.

What counts as progress: A representation argument covering every seven-vertex graph, or a counterexample; proving this case does not settle the question in all dimensions.

How the problem developed

8 Feb 2018 · Open problem [1]
Peter Frankl, Andrey Kupavskii and Konrad J. Swanepoel Asked whether every graph on 2d+1 vertices, or its complement, has a unit-distance representation in R^d.
24 Sept 2026 · Reported claim [2]
Dishah Posted a Lean-checked proof for the d=3 instance: every graph on seven vertices or its complement has a unit-distance representation in R³.

AI contribution

AI-led Lean proof settles a seven-vertex unit-distance case

For every simple graph G on seven vertices, either G or its complement has an injective unit-distance representation in Euclidean R³, where every edge has length one and nonedges are unconstrained. This proves the d=3 case of Frankl–Kupavskii–Swanepoel Problem 2; their general 2d+1-vertex question remains open. Combining with the published lower bound gives f_D(7)=3, although the lower bound is outside the formal target.

AI involvementAI-led

ImportanceModest

Technical verificationFormal (Lean 4 with Comparator and NanoDa)

Human understandingFew