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

2 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 87

References:

Imports (1)
  1. theorem Erdos87.erdos_87.parts.i Let $0 < \epsilon < 1$ sorry line 45 source

    Source documentation

    Let $0 < \epsilon < 1$. Is it true that, if $k$ is sufficiently large, then $$R(G) > (1-\epsilon)^k R(k)$$ for every graph $G$ with chromatic number $\chi(G)=k$?

    The restriction $\epsilon < 1$ excludes negative bases in $(1-\epsilon)^k$.

    This problem is #12 in Ramsey Theory in the graphs problem collection.

    depends on sorry what this means

    Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, LT.lt, Filter.Eventually, Nat, Fintype, SimpleGraph, Eq, ENat, SimpleGraph.chromaticNumber, SimpleGraph.diagonalGraphRamsey, HMul.hMul, HPow.hPow, HSub.hSub, SimpleGraph.diagonalRamsey, Filter.atTop

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

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_87.parts.i : answer(sorry) ↔
    ∀ ε > (0 : ℝ), ε < 1 → ∀ᶠ k : ℕ in atTop,
      ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.chromaticNumber = (k : ℕ∞) →
        (SimpleGraph.diagonalGraphRamsey G : ℝ) >
          (1 - ε) ^ k * (SimpleGraph.diagonalRamsey k : ℝ) := by
…

    Mentions: SimpleGraph.diagonalGraphRamsey, SimpleGraph.diagonalRamsey

  2. theorem Erdos87.erdos_87.parts.ii Even stronger, is there some $c > 0$ such that, for all large $k$, $$R(G) > c R(k)$$ for every graph $G$ with chromatic number $\chi(G)=k$? sorry line 60 source

    Source documentation

    Even stronger, is there some $c > 0$ such that, for all large $k$, $$R(G) > c R(k)$$ for every graph $G$ with chromatic number $\chi(G)=k$?

    This problem is #13 in Ramsey Theory in the graphs problem collection.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Fintype, SimpleGraph, Eq, ENat, SimpleGraph.chromaticNumber, SimpleGraph.diagonalGraphRamsey, HMul.hMul, SimpleGraph.diagonalRamsey, Filter.atTop

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

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_87.parts.ii : answer(sorry) ↔
    ∃ c > (0 : ℝ), ∀ᶠ k : ℕ in atTop,
      ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.chromaticNumber = (k : ℕ∞) →
        (SimpleGraph.diagonalGraphRamsey G : ℝ) > c * (SimpleGraph.diagonalRamsey k : ℝ) := by
…

    Mentions: c, SimpleGraph.diagonalGraphRamsey, SimpleGraph.diagonalRamsey