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

The smallest number of edges in a graph of dimension $4$ is $9$ .

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

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.