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 statement5 of 5

The smallest number of edges in a graph of dimension $4$ is achieved solely by $K_{3,3}$ .

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

1∀ (n : ℕ) (G : SimpleGraph (Fin n)),2  G.HasDimension 4 →3    G.edgeSet.ncard = 9 → (∀ (v : Fin n), ∃ w, G.Adj v w) → Nonempty (G ≃g completeBipartiteGraph (Fin 3) (Fin 3))

SolvedStatement only, no proof

Sources

Search problems.science