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

12 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 168

Reference: erdosproblems.com/168

Imports (1)
  1. def Erdos168.NonTernary Say a finite set of natural numbers is non ternary if it contains no 3-term arithmetic progression of the form n, 2n, 3n line 34 source

    Source documentation

    Say a finite set of natural numbers is non ternary if it contains no 3-term arithmetic progression of the form n, 2n, 3n.

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

    Statement uses: Finset, Nat

    Proof uses: Or, Not, Membership.mem, HMul.hMul, OfNat.ofNat

    5 instances, coercions and auxiliary constants left out.

    def NonTernary (S : Finset ℕ) : Prop := ∀ n : ℕ, n ∉ S ∨ 2*n ∉ S ∨ 3*n ∉ S
  2. def Erdos168.IntervalNonTernarySets IntervalNonTernarySets N is the (fin)set of non ternary subsets of {1,...,N} line 38 source

    Source documentation

    IntervalNonTernarySets N is the (fin)set of non ternary subsets of {1,...,N}. The advantage of defining it as below is that some proofs (e.g. that of F 3 = 2) become rfl.

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

    Statement uses: Nat, Finset

    Proof uses: Finset.filter, Membership.mem, Finset.Icc, OfNat.ofNat, HDiv.hDiv, Or, Not, HMul.hMul, Finset.powerset

    14 instances, coercions and auxiliary constants left out.

    def IntervalNonTernarySets (N : ℕ) : Finset (Finset ℕ) :=
…
  3. abbrev Erdos168.F F N is the size of the largest non ternary subset of {1,...,N} line 43 source

    Source documentation

    F N is the size of the largest non ternary subset of {1,...,N}.

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

    Statement uses: Nat

    Proof uses: Finset.sup, Finset, Erdos168.IntervalNonTernarySets, Finset.card

    3 instances, coercions and auxiliary constants left out.

    abbrev F (N : ℕ) : ℕ := (IntervalNonTernarySets N).sup Finset.card
…

    Mentions: Erdos168.IntervalNonTernarySets

  4. lemma Erdos168.F_0 line 46 source

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

    Statement uses: Eq, Nat, Erdos168.F, OfNat.ofNat

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  5. lemma Erdos168.F_1 line 49 source

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

    Statement uses: Eq, Nat, Erdos168.F, OfNat.ofNat

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  6. lemma Erdos168.F_2 line 52 source

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

    Statement uses: Eq, Nat, Erdos168.F, OfNat.ofNat

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  7. lemma Erdos168.F_3 line 55 source

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

    Statement uses: Eq, Nat, Erdos168.F, OfNat.ofNat

    Proof uses: rfl

    2 instances, coercions and auxiliary constants left out.

  8. lemma Erdos168.mem_IntervalNonTernarySets_iff Sanity check: elements of IntervalNonTernarySets N are precisely non ternary subsets of {1,...,N} line 62 source

    Source documentation

    Sanity check: elements of IntervalNonTernarySets N are precisely non ternary subsets of {1,...,N}

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

    Statement uses: Nat, Finset, Iff, Membership.mem, Erdos168.IntervalNonTernarySets, And, Erdos168.NonTernary, LE.le, Finset.Icc, OfNat.ofNat

    Proof uses: Iff.intro, Eq.mpr, HMul.hMul, Not, id, Eq, Eq.trans, True, congr, congrArg, forall_congr, Or, mul_comm, implies_congr, Eq.refl, propext, Finset.subset_iff, implies_congr_ctx, eq_true, Eq.mp and 14 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma mem_IntervalNonTernarySets_iff (N : ℕ) (S : Finset ℕ) :
    S ∈ IntervalNonTernarySets N ↔ NonTernary S ∧ S ⊆ Finset.Icc 1 N := by
…

    Mentions: Erdos168.IntervalNonTernarySets, Erdos168.NonTernary

  9. lemma Erdos168.F_eq_card Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S line 74 source

    Source documentation

    Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S

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

    Statement uses: Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, Erdos168.NonTernary, Finset.card, Eq, Erdos168.F

    Proof uses: Membership.mem, Erdos168.IntervalNonTernarySets, Eq.mpr, And, id, congrArg, propext, Erdos168.mem_IntervalNonTernarySets_iff, And.intro, Finset.le_sup, Finset.sup_le, Decidable.byContradiction, Not, And.right, Eq.mp, And.left, LT.lt

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

    lemma F_eq_card (N : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 N) (hS' : NonTernary S)
    (hS'' : ∀ T, T ⊆ Finset.Icc 1 N → NonTernary T → S.card ≤ T.card → T.card = S.card) :
    F N = S.card := by
…

    Mentions: Erdos168.NonTernary, Erdos168.F

  10. theorem Erdos168.erdos_168.parts.i What is the limit $F(N)/N$ as $N \to \infty$? sorry line 92 source

    Source documentation

    What is the limit $F(N)/N$ as $N \to \infty$?

    depends on sorry what this means

    Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Erdos168.F, Filter.atTop, nhds, sorryAx, Bool.false

    Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_168.parts.i :
    Filter.Tendsto (fun N => (F N / N : ℝ)) Filter.atTop (𝓝 answer(sorry)) := by
…

    Mentions: Erdos168.F

  11. theorem Erdos168.erdos_168.parts.ii Is the limit $F(N)/N$ as $N \to \infty$ irrational? sorry line 98 source

    Source documentation

    Is the limit $F(N)/N$ as $N \to \infty$ irrational?

    depends on sorry what this means

    Statement uses: Iff, True, Irrational, Filter.limsup, Real, Nat, HDiv.hDiv, Erdos168.F, Filter.atTop

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

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_168.parts.ii : answer(sorry) ↔
    Irrational (Filter.atTop.limsup (fun N => (F N / N : ℝ))) := by
…

    Mentions: Erdos168.F

  12. theorem Erdos168.erdos_168.variants.limit_exists The limit $F(N)/N$ as $N \to \infty$ exists sorry line 104 source

    Source documentation

    The limit $F(N)/N$ as $N \to \infty$ exists. (proved by Graham, Spencer, and Witsenhausen)

    depends on sorry what this means

    Statement uses: Exists, Real, Filter.Tendsto, Nat, HDiv.hDiv, Erdos168.F, Filter.atTop, nhds

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

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_168.variants.limit_exists :
    ∃ x, Filter.Tendsto (fun N => (F N / N : ℝ)) Filter.atTop (𝓝 x) := by
…

    Mentions: Erdos168.F