Erdős problem 1007 · problems.science

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

Sources

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

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

1007.lean

Retained formal statement2 of 5

The smallest number of edges in a graph of dimension $5$ is $15$ .

FormalConjectures/ErdosProblems/1007.leanErdos1007.erdos_1007.variants.dimension_five1 lineExact file

1IsLeast {m | ∃ n G, G.HasDimension 5 ∧ G.edgeSet.ncard = m} 15

SolvedStatement only, no proof