FormalConjectures/ErdosProblems/781.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, 3 contain sorry, 0 declared as axioms

Erdős Problem 781

References:

Imports (1)
  1. def Erdos781.IsDescendingWave A $k$-term descending wave is a sequence $x_1<\cdots <x_k$ such that, for $1<j<k$, $x_j \geq \frac{x_{j+1}+x_{j-1}}{2}$ line 39 source

    Source documentation

    A $k$-term descending wave is a sequence $x_1<\cdots <x_k$ such that, for $1<j<k$, $x_j \geq \frac{x_{j+1}+x_{j-1}}{2}$.

    standard axioms: propext what this means

    Statement uses: Nat, Fin

    Proof uses: And, StrictMono, Eq, HAdd.hAdd, OfNat.ofNat, LE.le, HMul.hMul

    10 instances, coercions and auxiliary constants left out.

    def IsDescendingWave {k : ℕ} (x : Fin k → ℕ) : Prop :=
…
  2. def Erdos781.f f k is the minimal n such that any $2$-colouring of $\{1,\ldots,n\}$ (identified with Fin n) contains a monochromatic $k$-term descending wave line 45 source

    Source documentation

    f k is the minimal n such that any $2$-colouring of $\{1,\ldots,n\}$ (identified with Fin n) contains a monochromatic $k$-term descending wave.

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

    Statement uses: Nat

    Proof uses: InfSet.sInf, Set.ofPred, Fin, OfNat.ofNat, Exists, And, Erdos781.IsDescendingWave, Eq

    3 instances, coercions and auxiliary constants left out.

    noncomputable def f (k : ℕ) : ℕ :=
…
  3. theorem Erdos781.erdos_781.parts.i sorry line 60 source

    depends on sorry what this means

    Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos781.f, HPow.hPow, OfNat.ofNat

    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.

  4. theorem Erdos781.erdos_781.parts.ii sorry line 70 source

    depends on sorry what this means

    Statement uses: Iff, False, Nat, GE.ge, OfNat.ofNat, Eq, Erdos781.f, HAdd.hAdd, HSub.hSub, 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.

  5. theorem Erdos781.erdos_781.variants.brown_erdos_freedman Brown, Erdős, and Freedman [BEF90] proved $k^2-k+1\leq f(k) \leq \frac{k^3-4k+9}{3}$ sorry line 75 source

    Source documentation

    Brown, Erdős, and Freedman [BEF90] proved $k^2-k+1\leq f(k) \leq \frac{k^3-4k+9}{3}$.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, And, HAdd.hAdd, HSub.hSub, HPow.hPow, Erdos781.f, Rat, HDiv.hDiv, HMul.hMul

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

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_781.variants.brown_erdos_freedman (k : ℕ) (hk : 1 ≤ k) :
    k ^ 2 - k + 1 ≤ f k ∧ (f k : ℚ) ≤ (k ^ 3 - 4 * k + 9) / 3 := by
…

    Mentions: Erdos781.f