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

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 61 -- Erdős–Hajnal Conjecture

Reference: erdosproblems.com/61

Imports (1)
Imported by 2 files
  1. def Erdos61.IsErdosHajnalLowerBound For a graph $H$, consider all graphs $G$ that do not contain $H$ as an induced subgraph line 39 source

    Source comment

    For a graph $H$, consider all graphs $G$ that do not contain $H$ as an induced subgraph. We would like to find a lower bound $f(n)$ such that every such $G$ on $n$ vertices has a clique or independent set of size $\ge f(n)$ for sufficiently large $n$.

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, Nat, Real

    Proof uses: Filter.Eventually, Fin, Not, Exists, Function.Embedding, Eq, SimpleGraph.comap, Or, GE.ge, SimpleGraph.indepNum, SimpleGraph.cliqueNum, Filter.atTop

    6 instances, coercions and auxiliary constants left out.

    def IsErdosHajnalLowerBound {α : Type*} [Fintype α] [DecidableEq α]
  (H : SimpleGraph α) (f : ℕ → ℝ) : Prop :=
…
  2. theorem Erdos61.erdos_61 The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation sorry line 49 source

    Source documentation

    The Erdős–Hajnal Conjecture states that there is a constant $c(H) > 0$ for each $H$ such that we can take $f(n) = n^{c(H)}$ in the above formulation.

    depends on sorry what this means

    Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, Exists, Real, And, GT.gt, OfNat.ofNat, Erdos61.IsErdosHajnalLowerBound, Nat, HPow.hPow

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_61 :
    answer(sorry) ↔ ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => (n : ℝ) ^ c) := by
…

    Mentions: c, Erdos61.IsErdosHajnalLowerBound

  3. theorem Erdos61.erdos_61.variants.erha89 Erdős and Hajnal [ErHa89] proved that we can take $f(n) = \exp(c_H \sqrt{\log n})$ for some constant $c_H > 0$ depending on $H$ sorry line 61 source

    Source documentation

    Erdős and Hajnal [ErHa89] proved that we can take $f(n) = \exp(c_H \sqrt{\log n})$ for some constant $c_H > 0$ depending on $H$.

    [ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, Exists, Real, And, GT.gt, OfNat.ofNat, Erdos61.IsErdosHajnalLowerBound, Nat, Real.exp, HMul.hMul, Real.sqrt, Real.log

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_61.variants.erha89 :
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => exp (c * sqrt (log n))) := by
…

    Mentions: c, Erdos61.IsErdosHajnalLowerBound

  4. theorem Erdos61.erdos_61.variants.bnss23 Bucić, Nguyen, Scott, and Seymour [BNSS23] improved this to $f(n) = \exp(c_H \sqrt{\log n \log \log n})$ for some constant $c_H > 0$ depending on $H$ sorry line 73 source

    Source documentation

    Bucić, Nguyen, Scott, and Seymour [BNSS23] improved this to $f(n) = \exp(c_H \sqrt{\log n \log \log n})$ for some constant $c_H > 0$ depending on $H$.

    [BNSS23] Bucić, M. and Nguyen, T. and Scott, A. and Seymour, P., A loglog step towards Erdos-Hajnal

    depends on sorry what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, Exists, Real, And, GT.gt, OfNat.ofNat, Erdos61.IsErdosHajnalLowerBound, Nat, Real.exp, HMul.hMul, Real.sqrt, Real.log

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_61.variants.bnss23 :
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => exp (c * sqrt (log n * log (log n)))) := by
…

    Mentions: c, Erdos61.IsErdosHajnalLowerBound

  5. theorem Erdos61.erdos_61.variants.p5 Documented declaration: p5 sorry line 87 source

    Source documentation

    Nguyen, Scott, and Seymour [NSS23] proved the conjecture for $H = P_5$, the path on five vertices: every $P_5$-free graph on $n$ vertices has a clique or independent set of polynomial size.

    [NSS23] Nguyen, T., Scott, A. and Seymour, P., Induced subgraph density. VII. The five-vertex path. arXiv:2312.15333

    L4DEL explanation

    Nguyen, Scott, and Seymour [NSS23] proved the conjecture for $H = P_5$, the path on five vertices: every $P_5$-free graph on $n$ vertices has a clique or independent set of polynomial size. [NSS23] Nguyen, T., Scott, A. and Seymour, P., Induced subgraph density. VII. The five-vertex path. arXiv:2312.15333

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Erdos61.IsErdosHajnalLowerBound, Fin, Nat, SimpleGraph.pathGraph, HPow.hPow

    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_61.variants.p5 :
    ∃ c > (0 : ℝ), IsErdosHajnalLowerBound (pathGraph 5) (fun n : ℕ => (n : ℝ) ^ c) := by
…

    Mentions: c, Erdos61.IsErdosHajnalLowerBound

  6. theorem Erdos61.erdos_61.variants.c5 Documented declaration: c5 sorry line 100 source

    Source documentation

    Chudnovsky, Scott, Seymour, and Spirkl [CSSS23] proved the conjecture for $H = C_5$, the cycle on five vertices: every graph with no induced five-cycle has a clique or independent set of polynomial size.

    [CSSS23] Chudnovsky, M., Scott, A., Seymour, P. and Spirkl, S., Erdős–Hajnal for graphs with no 5-hole. Proc. Lond. Math. Soc. (3) 126 (2023), 997–1014.

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Erdos61.IsErdosHajnalLowerBound, Fin, Nat, SimpleGraph.cycleGraph, HPow.hPow

    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_61.variants.c5 :
    ∃ c > (0 : ℝ), IsErdosHajnalLowerBound (cycleGraph 5) (fun n : ℕ => (n : ℝ) ^ c) := by
…

    Mentions: c, Erdos61.IsErdosHajnalLowerBound