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

Erdős Problem 332

Reference: erdosproblems.com/332

Imports (1)
Imported by 1 file
  1. def Erdos332.D_A The set of numbers $D(A)$ which occur infinitely often as $a_1 - a_2$ with $a_1, a_2 \in A$ line 35 source

    Source documentation

    The set of numbers $D(A)$ which occur infinitely often as $a_1 - a_2$ with $a_1, a_2 \in A$.

    no axioms what this means

    Statement uses: Set, Nat, Int

    Proof uses: Set.ofPred, Set.Infinite, Prod, Erdos332.D_A.match_1, And, Membership.mem, Eq, HSub.hSub

    5 instances, coercions and auxiliary constants left out.

    noncomputable def D_A (A : Set ℕ) : Set ℤ :=
…
  2. def Erdos332.HasBoundedGaps A set $S \subseteq \mathbb{Z}$ has bounded gaps if it is syndetic, meaning there is a uniform bound $M$ such that every interval of length $M$ contains an element of $S$ line 42 source

    Source documentation

    A set $S \subseteq \mathbb{Z}$ has bounded gaps if it is syndetic, meaning there is a uniform bound $M$ such that every interval of length $M$ contains an element of $S$.

    no axioms what this means

    Statement uses: Set, Int

    Proof uses: Exists, Nat, And, GT.gt, OfNat.ofNat, Membership.mem, LE.le, LT.lt, HAdd.hAdd

    9 instances, coercions and auxiliary constants left out.

    def HasBoundedGaps (S : Set ℤ) : Prop :=
…
  3. theorem Erdos332.erdos_332 Let $A\subseteq \mathbb{N}$ and $D(A)$ be the set of those numbers which occur infinitely often as $a_1 - a_2$ with $a_1, a_2\in A$ sorry line 55 source

    Source documentation

    Let $A\subseteq \mathbb{N}$ and $D(A)$ be the set of those numbers which occur infinitely often as $a_1 - a_2$ with $a_1, a_2\in A$. What conditions on $A$ are sufficient to ensure $D(A)$ has bounded gaps?

    This is formalised here using the answer(sorry) mechanism. In order to solve this problem one has to provide what the sufficient conditions are, and proof that they imply the desired condition. If the condition is a solution to the problem is up to human judgement.

    depends on sorry what this means

    Statement uses: Set, Nat, sorryAx, Bool.false, Erdos332.HasBoundedGaps, Erdos332.D_A

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

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_332 (A : Set ℕ) : (answer(sorry) : Set ℕ → Prop) A → HasBoundedGaps (D_A A) := by
…

    Mentions: Erdos332.HasBoundedGaps, Erdos332.D_A