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

Open selected source

FormalConjectures/ErdosProblems/

1007.lean

Retained formal statement3 of 5

The smallest number of edges in a graph of dimension $5$ is achieved by $K_6$ and $K_{1,3,3}$ .

FormalConjectures/ErdosProblems/1007.leanErdos1007.erdos_1007.variants.dimension_five_extremal2 linesExact file

1((SimpleGraph.completeGraph (Fin 6)).HasDimension 5 ∧ (SimpleGraph.completeGraph (Fin 6)).edgeSet.ncard = 15) ∧2  Erdos1007.K133.HasDimension 5 ∧ Erdos1007.K133.edgeSet.ncard = 15

SolvedStatement only, no proof

Sources

Search problems.science