Skip to content

Erdős problem 1007

The dimension of a graph GG is the minimal nn such that GG can be embedded in Rn\mathbb{R}^n such that every edge of GG is a unit line segment.

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1007.lean

Retained formal statement1 of 5

The dimension of a graph GG is the minimal nn such that GG can be embedded in Rn\mathbb{R}^n such that every edge of GG is a unit line segment.

What is the smallest number of edges in a graph with dimension 44?

The smallest number of edges is 99, achieved solely by K3,3K_{3,3}, proved by House [Ho13]. An alternative proof was given by Chaffee and Noble [ChNo16], who also prove that the smallest number of edges in a graph of dimension 55 is 1515 (achieved by K6K_6 and K1,3,3K_{1,3,3}).

FormalConjectures/ErdosProblems/1007.leanErdos1007.erdos_10071 lineExact file
IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorry
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page