Sierpiński numbers

References:

• Wikipedia, Sierpiński number
• [Si60] Sierpiński, W., Elementary Theory of Numbers. Państwowe Wydawnictwo Naukowe, Warsaw (1960).

A positive odd integer $k$ is a Sierpiński number if $k \cdot 2^n + 1$ is composite for all natural numbers $n$.

def Nat.IsSierpinskiNumber (k : ℕ) : Prop

A positive odd integer $k$ is a Sierpiński number if $k \cdot 2^n + 1$ is composite for all natural numbers $n$. In other words, every member of the set $\{k \cdot 2^n + 1 : n \in \mathbb{N}\}$ is composite.

Equations

• k.IsSierpinskiNumber = (¬2 ∣ k ∧ ∀ (n : ℕ), (k * 2 ^ n + 1).Composite)