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

Reference: erdosproblems.com/817

Imports (1)
  1. def Erdos817.g line 39 source

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

    Statement uses: Nat

    Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, OfNat.ofNat, Eq, Finset.card, Set, Membership.mem, Finset.powerset, Finset.sum, Set.IsAPOfLengthFree, ENat

    13 instances, coercions and auxiliary constants left out.

  2. theorem Erdos817.erdos_817 Let $k \geq 3$ sorry line 54 source

    Source documentation

    Let $k \geq 3$. Define $g_k(n)$ to be the minimal $N$ such that $\{1, ..., N\}$ contains some $A$ of size $|A| = n$ such that $$ \langle A\rangle = \left\{\sum_{a \in A} \epsilon_a a : \epsilon_a \in\{0, 1\}\right\} $$ contains no non-trivial $k$-term arithmetic progression. Estimate $g_k(n)$. In particular, is it true that $$ g_3(n) \gg 3^n $$

    depends on sorry what this means

    Statement uses: Iff, True, Asymptotics.IsBigO, Nat, Real, Filter.atTop, HPow.hPow, OfNat.ofNat, Erdos817.g

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

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_817 :
    answer(sorry) ↔ (fun n => (3 ^ n : ℝ)) =O[atTop] fun n => (g 3 n : ℝ) := by
…

    Mentions: Erdos817.g

  3. theorem Erdos817.erdos_817.variants.bdd_power A problem of Erdős and Sárközy who proved $$ g_3(n) \gg \frac{3^n}{n^{O(1)}}. $$ sorry line 63 source

    Source documentation

    A problem of Erdős and Sárközy who proved $$ g_3(n) \gg \frac{3^n}{n^{O(1)}}. $$

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, HDiv.hDiv, HPow.hPow, Erdos817.g

    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_817.variants.bdd_power : ∃ O > (0 : ℝ),
    (fun (n : ℕ) => (3 ^ n : ℝ) / n ^ O) =O[atTop] fun n => (g 3 n : ℝ) := by
…

    Mentions: Erdos817.g