FormalConjectures/ErdosProblems/617.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

4 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 617

References:

Imports (1)
Imported by 1 file
  1. theorem Erdos617.erdos_617 Let $r\geq 3$ sorry line 42 source

    Source documentation

    Let $r\geq 3$. If the edges of $K_{r^2+1}$ are $r$-coloured then there exist $r+1$ vertices with at least one colour missing on the edges of the induced $K_{r+1}$.

    In other words, there is no balanced colouring.

    A conjecture of Erdős and Gyárfás [ErGy99].

    depends on sorry what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, Fintype, DecidableEq, Eq, Fintype.card, HAdd.hAdd, HPow.hPow, Sym2, Fin, Exists, Finset, And, Finset.card, Membership.mem, Ne, Sym2.mk

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) :
    ∃ (S : Finset V) (k : Fin r),
      S.card = r + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k := by
…
  2. theorem Erdos617.erdos_617.variants.r_eq_3 Erdős and Gyárfás [ErGy99] proved the conjecture for $r=3$ sorry line 53 source

    Source documentation

    Erdős and Gyárfás [ErGy99] proved the conjecture for $r=3$.

    depends on sorry what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, Fintype, DecidableEq, Eq, Fintype.card, HAdd.hAdd, HPow.hPow, Sym2, Fin, Exists, Finset, And, Finset.card, Membership.mem, Ne, Sym2.mk

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_617.variants.r_eq_3 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = 3^2 + 1) (coloring : Sym2 V → Fin 3) :
    ∃ (S : Finset V) (k : Fin 3),
      S.card = 3 + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k := by
…
  3. theorem Erdos617.erdos_617.variants.r_eq_4 Erdős and Gyárfás [ErGy99] proved the conjecture for $r=4$ sorry line 64 source

    Source documentation

    Erdős and Gyárfás [ErGy99] proved the conjecture for $r=4$.

    depends on sorry what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, Fintype, DecidableEq, Eq, Fintype.card, HAdd.hAdd, HPow.hPow, Sym2, Fin, Exists, Finset, And, Finset.card, Membership.mem, Ne, Sym2.mk

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_617.variants.r_eq_4 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = 4^2 + 1) (coloring : Sym2 V → Fin 4) :
    ∃ (S : Finset V) (k : Fin 4),
      S.card = 4 + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k := by
…
  4. theorem Erdos617.erdos_617.variants.r2 Erdős and Gyárfás [ErGy99] showed this property fails for infinitely many $r$ if we replace $r^2+1$ by $r^2$ sorry line 76 source

    Source documentation

    Erdős and Gyárfás [ErGy99] showed this property fails for infinitely many $r$ if we replace $r^2+1$ by $r^2$.

    depends on sorry what this means

    Statement uses: Set.Infinite, Nat, Set.ofPred, Exists, Fintype, DecidableEq, And, Eq, Fintype.card, HPow.hPow, OfNat.ofNat, Sym2, Fin, Finset, Finset.card, HAdd.hAdd, Membership.mem, Ne, Sym2.mk

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

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_617.variants.r2 :
    {r : ℕ | ∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V), Fintype.card V = r^2 ∧
      ∃ (coloring : Sym2 V → Fin r),
        ∀ (S : Finset V), S.card = r + 1 →
          ∀ (k : Fin r), ∃ u ∈ S, ∃ v ∈ S, u ≠ v ∧ coloring s(u, v) = k}.Infinite := by
…