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

8 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 302

References:

Imports (1)
  1. def Erdos302.NoUnitFractionTriple A finite set $A$ of positive integers admits no solution to $\frac{1}{a} = \frac{1}{b} + \frac{1}{c}$ with $a, b, c$ distinct elements of $A$ line 43 source

    Source documentation

    A finite set $A$ of positive integers admits no solution to $\frac{1}{a} = \frac{1}{b} + \frac{1}{c}$ with $a, b, c$ distinct elements of $A$.

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

    Statement uses: Finset, Nat

    Proof uses: Membership.mem, Ne, Rat, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd

    9 instances, coercions and auxiliary constants left out.

    def NoUnitFractionTriple (A : Finset ℕ) : Prop :=
…
  2. def Erdos302.IsMaxNoTripleCard $f N$ is the size of the largest $A ⊆ \{1, …, N\}$ containing no solution to $\frac{1}{a} = \frac{1}{b} + \frac{1}{c}$ with distinct $a, b, c ∈ A$ line 51 source

    Source documentation

    $f N$ is the size of the largest $A ⊆ \{1, …, N\}$ containing no solution to $\frac{1}{a} = \frac{1}{b} + \frac{1}{c}$ with distinct $a, b, c ∈ A$.

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

    Statement uses: Nat

    Proof uses: IsGreatest, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, OfNat.ofNat, Erdos302.NoUnitFractionTriple, Eq, Finset.card

    7 instances, coercions and auxiliary constants left out.

    def IsMaxNoTripleCard (N m : ℕ) : Prop :=
…
  3. theorem Erdos302.erdos_302.parts.i Let $f(N)$ be the size of the largest $A\subseteq \{1,\ldots,N\}$ such that there are no solutions to $$\frac{1}{a}= \frac{1}{b}+\frac{1}{c}$$ with distinct $a,b,c\in A$? sorry line 63 source

    Source documentation

    Let $f(N)$ be the size of the largest $A\subseteq \{1,\ldots,N\}$ such that there are no solutions to $$\frac{1}{a}= \frac{1}{b}+\frac{1}{c}$$ with distinct $a,b,c\in A$? Estimate $f(N)$.

    The colouring version of this is [303], which was solved by Brown and Rödl [BrRo91].

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Filter.Tendsto, Real, HDiv.hDiv, 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_302.parts.i (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N)) :
    Tendsto (fun N : ℕ => (f N : ℝ) / N) atTop (𝓝 answer(sorry)) := by
…

    Mentions: Erdos302.IsMaxNoTripleCard

  4. theorem Erdos302.erdos_302.parts.ii In particular, is $f(N)=(\tfrac{1}{2}+o(1))N$? sorry line 74 source

    Source documentation

    In particular, is $f(N)=(\tfrac{1}{2}+o(1))N$?

    This is false: it is contradicted by Cambie's lower bound of $(5/8+o(1))N$ recorded below, since $5/8 > 1/2$.

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Not, Filter.Tendsto, Real, HDiv.hDiv, Filter.atTop, nhds, OfNat.ofNat

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

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_302.parts.ii (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N)) :
    ¬ Tendsto (fun N : ℕ => (f N : ℝ) / N) atTop (𝓝 ((1 : ℝ) / 2)) := by
…

    Mentions: Erdos302.IsMaxNoTripleCard

  5. theorem Erdos302.erdos_302.variants.lower_half One can take either $A$ to be all odd integers in $[1,N]$ or all integers in $[N/2,N]$ to show $f(N)\geq (1/2+o(1))N$ sorry line 83 source

    Source documentation

    One can take either $A$ to be all odd integers in $[1,N]$ or all integers in $[N/2,N]$ to show $f(N)\geq (1/2+o(1))N$.

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Real, LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, Filter.atTop

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

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_302.variants.lower_half (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ((1 : ℝ) / 2 - ε) * N ≤ f N := by
…

    Mentions: Erdos302.IsMaxNoTripleCard

  6. theorem Erdos302.erdos_302.variants.lower_five_eighths Stijn Cambie has observed that $$f(N)\geq (5/8+o(1))N,$$ taking $A$ to be all odd integers $\leq N/4$ and all integers in $[N/2,N]$ sorry line 94 source

    Source documentation

    Stijn Cambie has observed that $$f(N)\geq (5/8+o(1))N,$$ taking $A$ to be all odd integers $\leq N/4$ and all integers in $[N/2,N]$.

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Real, LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, 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_302.variants.lower_five_eighths (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, ((5 : ℝ) / 8 - ε) * N ≤ f N := by
…

    Mentions: Erdos302.IsMaxNoTripleCard

  7. theorem Erdos302.erdos_302.variants.upper_nine_tenths Wouter van Doorn has proved [va25] that $$f(N) \leq (9/10+o(1))N.$$ sorry line 104 source

    Source documentation

    Wouter van Doorn has proved [va25] that $$f(N) \leq (9/10+o(1))N.$$

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Real, LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, HDiv.hDiv, 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_302.variants.upper_nine_tenths (f : ℕ → ℕ) (hf : ∀ N, IsMaxNoTripleCard N (f N))
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ N : ℕ in atTop, (f N : ℝ) ≤ ((9 : ℝ) / 10 + ε) * N := by
…

    Mentions: Erdos302.IsMaxNoTripleCard

  8. theorem Erdos302.erdos_302.variants.upper_0_8461739827964010 sorry line 117 source

    depends on sorry what this means

    Statement uses: Nat, Erdos302.IsMaxNoTripleCard, Real, LT.lt, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, HDiv.hDiv, 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.