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

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

Source providers

Erdős Problems1
locator only
Formal Conjectures5
statement retained
VibeMathed0
not observed here
PLBY Lean proofs1
no statement retained
Jayyhk Erdős Lean1
no statement retained
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki2
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 1007.lean5