1. FormalConjectures
  2. ErdosProblems
  3. «1007»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 1007

References:

    erdosproblems.com/1007

    [ChNo16] Chaffee, Joe and Noble, Matt, Dimension 4 and dimension 5 graphs with minimum edge set. Australas. J. Combin. (2016), 327-333.

    [Ho13] House, Roger F., A 4-dimensional graph has at least 9 edges. Discrete Math. (2013), 1783-1789.

namespace Erdos1007open scoped EuclideanGeometryvariable {V : Type*}

The complete tripartite graph $K_{1,3,3}$.

abbrev K133 := SimpleGraph.completeMultipartiteGraph fun i : Fin 3 => Fin (![1, 3, 3] i)

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.

What is the smallest number of edges in a graph with dimension $4$?

Answer: The smallest number of edges is $9$, achieved solely by $K_{3,3}$, 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 $5$ is $15$ (achieved by $K_6$ and $K_{1,3,3}$).

@[category research solved, AMS 5 52, formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1007.lean"] theorem erdos_1007 : IsLeast {m | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G.HasDimension 4 ∧ G.edgeSet.ncard = m} 9 := ⊢ IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} 9 All goals completed! 🐙

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

@[category research solved, AMS 5 52] theorem erdos_1007.variants.dimension_four_extremal (n : ℕ) (G : SimpleGraph (Fin n)) (hdim : G.HasDimension 4) (hcard : G.edgeSet.ncard = 9) (hdeg : ∀ v : Fin n, ∃ w : Fin n, G.Adj v w) : Nonempty (G ≃g completeBipartiteGraph (Fin 3) (Fin 3)) := n:ℕG:SimpleGraph (Fin n)hdim:G.HasDimension 4hcard:G.edgeSet.ncard = 9hdeg:∀ (v : Fin n), ∃ w, G.Adj v w⊢ Nonempty (G ≃g completeBipartiteGraph (Fin 3) (Fin 3)) All goals completed! 🐙

The smallest number of edges in a graph of dimension $5$ is $15$.

@[category research solved, AMS 5 52] theorem erdos_1007.variants.dimension_five : IsLeast {m | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G.HasDimension 5 ∧ G.edgeSet.ncard = m} 15 := ⊢ IsLeast {m | ∃ n G, G.HasDimension 5 ∧ G.edgeSet.ncard = m} 15 All goals completed! 🐙

The smallest number of edges in a graph of dimension $5$ is achieved by $K_6$ and $K_{1,3,3}$.

@[category research solved, AMS 5 52] theorem erdos_1007.variants.dimension_five_extremal : ((SimpleGraph.completeGraph (Fin 6)).HasDimension 5 ∧ (SimpleGraph.completeGraph (Fin 6)).edgeSet.ncard = 15) ∧ (K133.HasDimension 5 ∧ K133.edgeSet.ncard = 15) := ⊢ ((SimpleGraph.completeGraph (Fin 6)).HasDimension 5 ∧ (SimpleGraph.completeGraph (Fin 6)).edgeSet.ncard = 15) ∧ K133.HasDimension 5 ∧ K133.edgeSet.ncard = 15 All goals completed! 🐙end Erdos1007