Erdős problem 1007
The dimension of a graph is the minimal such that can be embedded in such that every edge of is a unit line segment.
Sources
FormalConjectures/ErdosProblems/
1007.lean
Retained formal statement
The dimension of a graph is the minimal such that can be embedded in such that every edge of is a unit line segment.
What is the smallest number of edges in a graph with dimension ?
The smallest number of edges is , achieved solely by , 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 is (achieved by and ).
IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorrySolvedStatement only, no proof