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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1104

Reference: https://www.erdosproblems.com/1104

Imports (1)
  1. def Erdos1104.triangleFreeMaxChromatic Maximum chromatic number of a triangle-free graph on n vertices line 34 source

    Source documentation

    Maximum chromatic number of a triangle-free graph on n vertices.

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

    Statement uses: Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, SimpleGraph, Fin, And, SimpleGraph.CliqueFree, OfNat.ofNat, Eq, ENat, SimpleGraph.chromaticNumber

    4 instances, coercions and auxiliary constants left out.

    noncomputable def triangleFreeMaxChromatic (n : ℕ) : ℕ :=
…
  2. theorem Erdos1104.erdos_1104.variants.lower Lower bound (Hefty–Horn–King–Pfender 2025) sorry line 48 source

    Source documentation

    Lower bound (Hefty–Horn–King–Pfender 2025). $$ (1 - o(1)) \sqrt{\frac{n}{\log n}} \le f(n), $$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as triangleFreeMaxChromatic n.

    depends on sorry what this means

    Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HDiv.hDiv, HMul.hMul, HSub.hSub, Real.sqrt, Real.log, Erdos1104.triangleFreeMaxChromatic, Filter.atTop

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

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1104.variants.lower :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 - ε) * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ))
        ≤ (triangleFreeMaxChromatic n : ℝ) := by
…

    Mentions: Erdos1104.triangleFreeMaxChromatic

  3. theorem Erdos1104.erdos_1104.variants.upper Upper bound (Davies–Illingworth 2022) sorry line 63 source

    Source documentation

    Upper bound (Davies–Illingworth 2022). $$ f(n) \le (2 + o(1)) \sqrt{\frac{n}{\log n}}, $$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as triangleFreeMaxChromatic n.

    depends on sorry what this means

    Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Erdos1104.triangleFreeMaxChromatic, HDiv.hDiv, HMul.hMul, HAdd.hAdd, Real.sqrt, Real.log, Filter.atTop

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

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1104.variants.upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (triangleFreeMaxChromatic n : ℝ)
        ≤ (2 + ε) * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ)) := by
…

    Mentions: Erdos1104.triangleFreeMaxChromatic