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

References:

A positive odd integer $k$ is a Sierpiński number if $k \cdot 2^n + 1$ is composite for all $n \geq 0$. A covering set for $k$ is a finite set of primes $P$ such that every number of the form $k \cdot 2^n + 1$ is divisible by at least one prime in $P$.

Sierpiński (1960) proved that infinitely many Sierpiński numbers exist using covering systems. The smallest known Sierpiński number is 78557 (Selfridge). Erdős and Graham conjectured that there exist Sierpiński numbers with no finite covering set. A negative answer would imply infinitely many Fermat primes.

Note: The notion of a covering set for a Sierpiński number is closely related to a CoveringSystem of $\mathbb{Z}$ (see FormalConjecturesForMathlib.NumberTheory.CoveringSystem): a finite covering set of primes for $k$ works because the exponents $n$ for which each prime divides $k \cdot 2^n + 1$ form residue classes whose union covers all of $\mathbb{Z}$, i.e. a covering system.

See also Erdős Problems 203 and 276.

Imports (1)
Imported by 1 file
  1. def Erdos1113.HasFinitePrimeCoveringSet A covering set for a positive odd integer $k$ is a finite set of primes $P$ such that every number of the form $k \cdot 2^n + 1$ is divisible by at least one prime in $P$ line 59 source

    Source documentation

    A covering set for a positive odd integer $k$ is a finite set of primes $P$ such that every number of the form $k \cdot 2^n + 1$ is divisible by at least one prime in $P$.

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

    Statement uses: Nat

    Proof uses: Exists, Finset, And, Membership.mem, Nat.Prime, Dvd.dvd, HAdd.hAdd, HMul.hMul, HPow.hPow, OfNat.ofNat

    12 instances, coercions and auxiliary constants left out.

    def HasFinitePrimeCoveringSet (k : ℕ) : Prop :=
…
  2. theorem Erdos1113.erdos_1113.variants.infinitely_many_sierpinski sorry line 68 source

    depends on sorry what this means

    Statement uses: Set.Infinite, Nat, Set.ofPred, Nat.IsSierpinskiNumber

    Proof uses: sorryAx, Lean.Name, Bool.false, 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.

  3. theorem Erdos1113.erdos_1113 Erdős Problem 1113 sorry line 80 source

    Source documentation

    Erdős Problem 1113. Do there exist Sierpiński numbers that possess no finite covering set of primes?

    Erdős and Graham [ErGr80] conjectured that the answer is yes. A negative answer would imply that there are infinitely many Fermat primes.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, And, Nat.IsSierpinskiNumber, Not, Erdos1113.HasFinitePrimeCoveringSet

    Proof uses: sorryAx, Lean.Name, Bool.false, 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_1113 :
    answer(sorry) ↔
      ∃ k, k.IsSierpinskiNumber ∧ ¬ HasFinitePrimeCoveringSet k := by
…

    Mentions: Erdos1113.HasFinitePrimeCoveringSet

  4. theorem Erdos1113.erdos_1113.variants.filaseta_finch_kozek Filaseta–Finch–Kozek conjecture (2008) sorry line 90 source

    Source documentation

    Filaseta–Finch–Kozek conjecture (2008). Every Sierpiński number is either a perfect power or possesses a finite covering set of primes.

    depends on sorry what this means

    Statement uses: Nat, Nat.IsSierpinskiNumber, Or, Nat.IsPerfectPower, Erdos1113.HasFinitePrimeCoveringSet

    Proof uses: sorryAx, Lean.Name, Bool.false, 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_1113.variants.filaseta_finch_kozek :
    ∀ k, k.IsSierpinskiNumber →
      k.IsPerfectPower ∨ HasFinitePrimeCoveringSet k := by
…

    Mentions: Erdos1113.HasFinitePrimeCoveringSet