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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 198

References:

Imports (1)
Imported by 1 file
  1. lemma Erdos198.baumgartner_strong Let $V$ be a vector space over the rationals and let $k$ be a fixed positive integer sorry line 43 source

    Source documentation

    Let $V$ be a vector space over the rationals and let $k$ be a fixed positive integer. Then there is a set $X_k \subseteq V$ such that $X_k$ meets every infinite arithmetic progression in $V$ but $X_k$ intersects every $k$-element arithmetic progression in at most two points.

    At the end of [Ba75] the author claims that by "slightly modifying the method of [his proof]", one can prove this.

    depends on sorry what this means

    Statement uses: AddCommGroup, Module, Rat, Nat, Exists, Set, And, Set.IsAPOfLength, Top.top, ENat, Set.Nonempty, Inter.inter, LE.le, Set.ncard, OfNat.ofNat

    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.

    lemma baumgartner_strong (V : Type*) [AddCommGroup V] [Module ℚ V] (k : ℕ) :
    ∃ X : Set V,
      (∀ Y, Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧
      (∀ Y, IsAPOfLength Y k → (X ∩ Y).ncard ≤ 2) := by
…
  2. lemma Erdos198.baumgartner_headline The statement for which Baumgartner actually writes a proof line 51 source

    Source documentation

    The statement for which Baumgartner actually writes a proof.

    depends on sorry what this means

    Statement uses: AddCommGroup, Module, Rat, Exists, Set, And, Set.IsAPOfLength, Top.top, ENat, Set.Nonempty, Inter.inter, OfNat.ofNat, Nat, LE.le, Set.ncard

    Proof uses: Erdos198.baumgartner_strong

    13 instances, coercions and auxiliary constants left out.

    lemma baumgartner_headline (V : Type*) [AddCommGroup V] [Module ℚ V] :
    ∃ X : Set V,
      (∀ Y, IsAPOfLength Y ⊤ → (X ∩ Y).Nonempty) ∧
      (∀ Y, IsAPOfLength Y 3 → (X ∩ Y).ncard ≤ 2) :=
…
  3. theorem Erdos198.erdos_198 sorry line 77 source

    depends on sorry what this means

    Statement uses: Iff, Set, Nat, IsSidon, Exists, And, Set.IsAPOfLength, Top.top, ENat, LE.le, Compl.compl, False

    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.

  4. theorem Erdos198.erdos_198.variants.concrete In fact one such sequence is $n! + n$ sorry line 89 source

    Source documentation

    In fact one such sequence is $n! + n$.

    This was found and proved by AlphaProof.

    It also found $(n + 1)! + n$.

    depends on sorry what this means

    Statement uses: Exists, Set, Nat, And, Eq, Set.ofPred, HAdd.hAdd, Nat.factorial, IsSidon, Set.IsAPOfLength, Top.top, ENat, Set.Nonempty, Inter.inter

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

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_198.variants.concrete :  ∃ (A : Set ℕ), A = {n ! + n | n} ∧
    IsSidon A ∧ (∀ Y, IsAPOfLength Y ⊤ → (A ∩ Y).Nonempty) := by
…

    Mentions: IsSidon