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

6 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 272

Reference: erdosproblems.com/272

Imports (1)
Imported by 1 file
  1. def Erdos272.IsArithInterSet Let $N \in\mathbb{N}$ line 36 source

    Source documentation

    Let $N \in\mathbb{N}$. We say that $\{A_1, ..., A_t\}\subseteq \mathcal{P}(\{1, \dots, N\})$ is an arithmetic intersection set if $A_i \cap A_j$ is a non-empty arithmetic progression for each $i \neq j$.

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

    Statement uses: Nat, Finset

    Proof uses: And, LE.le, Finset.powerset, Finset.Icc, OfNat.ofNat, Set.Pairwise, Exists, ENat, GT.gt, Set.IsAPOfLength, Inter.inter

    17 instances, coercions and auxiliary constants left out.

    def IsArithInterSet (N : ℕ) (A : Finset (Finset ℕ)) : Prop :=
…
  2. def Erdos272.maxArithInterCard For each $N > 0$, let $t$ be the largest size of an arithmetic intersection set line 42 source

    Source documentation

    For each $N > 0$, let $t$ be the largest size of an arithmetic intersection set.

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

    Statement uses: Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, Erdos272.IsArithInterSet, Eq, Finset.card

    1 instances, coercions and auxiliary constants left out.

    noncomputable def maxArithInterCard (N : ℕ) : ℕ :=
…
  3. theorem Erdos272.erdos_272 Let $N\geq 1$ sorry line 51 source

    Source documentation

    Let $N\geq 1$. What is the largest $t$ such that there are $A_1,\ldots,A_t\subseteq \{1,\ldots,N\}$ with $A_i\cap A_j$ a non-empty arithmetic progression for all $i\neq j$?

    depends on sorry what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, Eq, Erdos272.maxArithInterCard, sorryAx, Bool.false

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

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_272 :
    ∀ N ≥ 1, maxArithInterCard N = (answer(sorry) : ℕ → ℕ) N := by
…

    Mentions: Erdos272.maxArithInterCard

  4. theorem Erdos272.erdos_272.variants.isBigO_sq Simonovits and Sós have shown that $t\ll N^2$ sorry line 59 source

    Source documentation

    Simonovits and Sós have shown that $t\ll N^2$.

    depends on sorry what this means

    Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, Erdos272.maxArithInterCard, 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.

    theorem erdos_272.variants.isBigO_sq :
    (fun N ↦ (maxArithInterCard N : ℝ)) =O[atTop] fun N ↦ (N : ℝ) ^ 2 := by
…

    Mentions: Erdos272.maxArithInterCard

  5. theorem Erdos272.erdos_272.variants.szabo Szabo showed that the maximal $t$ is equal to $$ \frac{N^2}{2} + O(N^{5/3}\log^3N). $$ sorry line 69 source

    Source documentation

    Szabo showed that the maximal $t$ is equal to $$ \frac{N^2}{2} + O(N^{5/3}\log^3N). $$

    depends on sorry what this means

    Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HSub.hSub, Erdos272.maxArithInterCard, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HMul.hMul, Real.log

    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_272.variants.szabo :
    (fun N ↦ (maxArithInterCard N - N ^ 2 / 2 : ℝ)) =O[atTop]
      fun N : ℕ ↦ N ^ ((5 : ℝ) /  3) * (Real.log N) ^ 3 := by
…

    Mentions: Erdos272.maxArithInterCard

  6. theorem Erdos272.erdos_272.variants.szabo_strong Szabo asks whether the maximal $t$ is given by $$ \frac{N^2}{2} + O(N) $$ sorry line 80 source

    Source documentation

    Szabo asks whether the maximal $t$ is given by $$ \frac{N^2}{2} + O(N) $$

    depends on sorry what this means

    Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HSub.hSub, Erdos272.maxArithInterCard, HDiv.hDiv, HPow.hPow, OfNat.ofNat

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_272.variants.szabo_strong :
    (fun N ↦ (maxArithInterCard N - N ^ 2 / 2 : ℝ)) =O[atTop] fun N : ℕ ↦ (N : ℝ) := by
…

    Mentions: Erdos272.maxArithInterCard