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

Reference: erdosproblems.com/1102

Imports (1)
  1. def Erdos1102.HasPropertyP Property P : A set $A ⊆ ℕ $ has property P, if for all $n ≥ 1$ the set $ \{a ∈ A | n + a\text{ is squarefree}\}$ is finite line 35 source

    Source documentation

    Property P : A set $A ⊆ ℕ $ has property P, if for all $n ≥ 1$ the set $ \{a ∈ A | n + a\text{ is squarefree}\}$ is finite.

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: GE.ge, OfNat.ofNat, Set.Finite, Set.ofPred, And, Membership.mem, Squarefree, HAdd.hAdd

    6 instances, coercions and auxiliary constants left out.

    def HasPropertyP (A : Set ℕ) : Prop :=
…
  2. def Erdos1102.HasPropertyQ Property Q : A set $A ⊆ ℕ $ has property Q, if the set $\{n ∈ ℕ | ∀ a ∈ A, n > a\text{ implies }n + a\text{ is squarefree}\}$ is infinite line 42 source

    Source documentation

    Property Q : A set $A ⊆ ℕ $ has property Q, if the set $\{n ∈ ℕ | ∀ a ∈ A, n > a\text{ implies }n + a\text{ is squarefree}\}$ is infinite.

    standard axioms: propext what this means

    Statement uses: Set, Nat

    Proof uses: Set.Infinite, Set.ofPred, Membership.mem, LT.lt, Squarefree, HAdd.hAdd

    5 instances, coercions and auxiliary constants left out.

    def HasPropertyQ (A : Set ℕ) : Prop :=
…
  3. theorem Erdos1102.erdos_1102.density_zero_of_P sorry line 52 source

    depends on sorry what this means

    Statement uses: Nat, StrictMono, Erdos1102.HasPropertyP, Set.range, Filter.Tendsto, Real, HDiv.hDiv, Filter.atTop

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Erdos1102.erdos_1102.exists_sequence_with_P sorry line 66 source

    depends on sorry what this means

    Statement uses: Nat, Filter.Tendsto, Filter.atTop, Ne, OfNat.ofNat, Exists, And, StrictMono, Erdos1102.HasPropertyP, Set.range, LE.le, Real, HDiv.hDiv

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

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Erdos1102.erdos_1102.upper_density_Q sorry line 79 source

    depends on sorry what this means

    Statement uses: Nat, StrictMono, Erdos1102.HasPropertyQ, Set.range, LE.le, Real, Filter.limsup, HDiv.hDiv, Filter.atTop, OfNat.ofNat, HPow.hPow, Real.pi

    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.

  6. theorem Erdos1102.erdos_1102.lower_density_Q_exists sorry line 93 source

    depends on sorry what this means

    Statement uses: Exists, Nat, And, StrictMono, Squarefree, Erdos1102.HasPropertyQ, Set.range, Filter.Tendsto, Real, HDiv.hDiv, Filter.atTop, nhds, OfNat.ofNat, HPow.hPow, Real.pi

    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.