FormalConjectures/ErdosProblems/424.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, 2 contain sorry, 0 declared as axioms

Erdős Problem 424: Sequence generated by $a_i a_j - 1$

References:

Imports (1)
Imported by 1 file
  1. def Erdos424.nextGeneration Defines the set of new numbers generated from a set A by the operation $x y - 1$ for $x \neq y$ line 41 source

    Source documentation

    Defines the set of new numbers generated from a set A by the operation $x y - 1$ for $x \neq y$.

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, Exists, And, Membership.mem, Ne, Eq, HSub.hSub, HMul.hMul, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

    def nextGeneration (A : Set ℕ) : Set ℕ :=
…
  2. def Erdos424.sequenceSet The sequence of sets $A_n$ where $A_0 = \{2, 3\}$ and $A_{n+1}$ is $A_n$ union all newly generated elements line 48 source

    Source documentation

    The sequence of sets $A_n$ where $A_0 = \{2, 3\}$ and $A_{n+1}$ is $A_n$ union all newly generated elements.

    no axioms what this means

    Statement uses: Nat, Set

    2 instances, coercions and auxiliary constants left out.

    def sequenceSet : ℕ → Set ℕ
  | 0 => {2, 3}
  | n + 1 => (sequenceSet n) ∪ (nextGeneration (sequenceSet n))

/-- The set of integers which eventually appear in the sequence, which is the union of all $A_n$. -/

    Mentions: Erdos424.nextGeneration

  3. def Erdos424.generatedSet The set of integers which eventually appear in the sequence, which is the union of all $A_n$ line 53 source

    Source documentation

    The set of integers which eventually appear in the sequence, which is the union of all $A_n$.

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.iUnion, Erdos424.sequenceSet

    def generatedSet : Set ℕ := ⋃ n : ℕ, sequenceSet n
…

    Mentions: Erdos424.sequenceSet

  4. theorem Erdos424.erdos_424 sorry line 72 source

    depends on sorry what this means

    Statement uses: Iff, True, LT.lt, Real, OfNat.ofNat, Set.lowerDensity, Nat, Erdos424.generatedSet, Set.univ

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Erdos424.erdos_424.variants.exact_density A literal interpretation of "positive density": the natural density of generatedSet exists (i.e. the lower and upper density agree) and is positive sorry line 80 source

    Source documentation

    A literal interpretation of "positive density": the natural density of generatedSet exists (i.e. the lower and upper density agree) and is positive.

    depends on sorry what this means

    Statement uses: Iff, True, Set.HasPosDensity, Nat, Erdos424.generatedSet, Set.univ

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

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_424.variants.exact_density : answer(sorry) ↔ generatedSet.HasPosDensity := by
…