Erdős problem 1007

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

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