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

References:

Imports (1)
Imported by 1 file
  1. theorem Erdos865.erdos_865 sorry line 55 source

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, LE.le, Finset.Icc, GE.ge, Finset.card, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Membership.mem, Ne, Filter.atTop

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

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. theorem Erdos865.erdos_865.variants.k2 It is a classical folklore fact that if $A\subseteq \{1,\ldots,2N\}$ has size $\geq N+2$ then there are distinct $a,b\in A$ such that $a+b\in A$, which establishes the $k=2$ case line 67 source

    Source documentation

    It is a classical folklore fact that if $A\subseteq \{1,\ldots,2N\}$ has size $\geq N+2$ then there are distinct $a,b\in A$ such that $a+b\in A$, which establishes the $k=2$ case.

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

    Statement uses: Nat, Finset, LE.le, Finset.Icc, OfNat.ofNat, HMul.hMul, GE.ge, Finset.card, HAdd.hAdd, Exists, And, Membership.mem, Ne

    Proof uses: Finset.Nonempty, Eq.mpr, LT.lt, id, Eq, congrArg, Eq.symm, propext, Finset.card_pos, Decidable.byContradiction, Not, Finset.max', rfl, Finset.max'_mem, Eq.mp, Finset.mem_Icc, Finset.erase, HSub.hSub, Finset.card_erase_of_mem, Nat.card_Icc and 8 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

    theorem erdos_865.variants.k2 (N : ℕ) :
    ∀ A ⊆ Icc 1 (2 * N), A.card ≥ N + 2 →
    ∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ a + b ∈ A := by
…
  3. def Erdos865.f line 100 source

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

    Statement uses: Nat

    Proof uses: InfSet.sInf, Set.ofPred, Finset, LE.le, Finset.Icc, OfNat.ofNat, GE.ge, Finset.card, Exists, And, Eq, Membership.mem, Ne, HAdd.hAdd

    12 instances, coercions and auxiliary constants left out.

  4. theorem Erdos865.erdos_865.variants.sos Documented declaration: sos sorry line 111 source

    Source documentation

    Erdős and Sós conjectured that $f_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N$, where $f_k(N)$ is the minimal size of a subset of $\{1, \dots, N\}$ guaranteeing $k$ elements have all pairwise sums in the set.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Asymptotics.IsEquivalent, Real, Filter.atTop, Erdos865.f, HMul.hMul, HDiv.hDiv, HAdd.hAdd, Finset.sum, Finset.Icc, HSub.hSub, HPow.hPow

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

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_865.variants.sos :
    ∀ᵉ (k : ℕ) (hk : 2 ≤ k),
    (fun N ↦ (f N k : ℝ)) ~[atTop] (fun N ↦ (1 / 2 : ℝ) * (1 + ∑ r ∈ Icc 1 (k - 2),
      (1 / 4 : ℝ) ^ r) * N) := by
…

    Mentions: Erdos865.f

  5. theorem Erdos865.erdos_865.variants.upper_bound Choi, Erdős, and Szemerédi [CES75] have proved that, for all sorry line 122 source

    Source documentation

    Choi, Erdős, and Szemerédi [CES75] have proved that, for all $k\geq 3$, there exists $\epsilon_k>0$ such that (for large enough $N$) $f_k(N)\leq \left(\frac{2}{3}-\epsilon_k\right)N$.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Real, And, GT.gt, Filter.Eventually, Erdos865.f, HMul.hMul, HSub.hSub, HDiv.hDiv, Filter.atTop

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

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_865.variants.upper_bound (k : ℕ) (hk : 3 ≤ k) :
    ∃ ε > 0, ∀ᶠ N in atTop, (f N k : ℝ) ≤ (2 / 3 - ε) * N := by
…

    Mentions: Erdos865.f