Skip to content

Erdős problem 1007

The dimension of a graph GG is the minimal nn such that GG can be embedded in Rn\mathbb{R}^n such that every edge of GG is a unit line segment.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1007.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1007.leanErdos1007.erdos_10071 lineExact file
IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorry
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1007
  • PLBY Lean proofsErdosProblems.Erdos1007

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page