FormalConjectures/ErdosProblems/1007.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 1007

References:

Imports (1)
  1. abbrev Erdos1007.K133 The complete tripartite graph $K_{1,3,3}$ line 40 source

    Source documentation

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

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, Sigma, Fin, OfNat.ofNat, Nat, Matrix.vecCons, Nat.succ, Matrix.vecEmpty

    Proof uses: SimpleGraph.completeMultipartiteGraph

    2 instances, coercions and auxiliary constants left out.

    abbrev K133 := SimpleGraph.completeMultipartiteGraph fun i : Fin 3 => Fin (![1, 3, 3] i)
…
  2. theorem Erdos1007.erdos_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 sorry line 53 source

    Source documentation

    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}$).

    depends on sorry what this means

    Statement uses: IsLeast, Nat, Set.ofPred, Exists, SimpleGraph, Fin, And, SimpleGraph.HasDimension, OfNat.ofNat, Eq, Set.ncard, Sym2, SimpleGraph.edgeSet

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_1007 :
    IsLeast {m | ∃ (n : ℕ) (G : SimpleGraph (Fin n)), G.HasDimension 4 ∧ G.edgeSet.ncard = m}
      9 := by
…
  3. theorem Erdos1007.erdos_1007.variants.dimension_four_extremal sorry line 64 source

    depends on sorry what this means

    Statement uses: Nat, SimpleGraph, Fin, SimpleGraph.HasDimension, OfNat.ofNat, Eq, Set.ncard, Sym2, SimpleGraph.edgeSet, Exists, SimpleGraph.Adj, Nonempty, SimpleGraph.Iso, Sum, completeBipartiteGraph

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  4. theorem Erdos1007.erdos_1007.variants.dimension_five sorry line 76 source

    depends on sorry what this means

    Statement uses: IsLeast, Nat, Set.ofPred, Exists, SimpleGraph, Fin, And, SimpleGraph.HasDimension, OfNat.ofNat, Eq, Set.ncard, Sym2, SimpleGraph.edgeSet

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  5. theorem Erdos1007.erdos_1007.variants.dimension_five_extremal sorry line 87 source

    depends on sorry what this means

    Statement uses: And, SimpleGraph.HasDimension, Fin, OfNat.ofNat, Nat, SimpleGraph.completeGraph, Eq, Set.ncard, Sym2, SimpleGraph.edgeSet, Sigma, Matrix.vecCons, Nat.succ, Matrix.vecEmpty, Erdos1007.K133

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.