FormalConjectures.Wikipedia.SierpinskiNumber

FormalConjectures
Wikipedia
SierpinskiNumber

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Sierpiński number

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$. In 1960, Sierpiński proved that there are infinitely many such numbers. John Selfridge proved in 1962 that 78557 is a Sierpiński number. It is conjectured to be the smallest.

Sierpiński problem

The Sierpiński problem asks: is 78557 the smallest Sierpiński number?

Prime Sierpiński problem

The prime Sierpiński problem asks: is 271129 the smallest prime Sierpiński number?

Extended Sierpiński problem

The extended Sierpiński problem asks: is 271129 the second-smallest Sierpiński number?

namespace SierpinskiNumber

Selfridge proved in 1962 that 78557 is a Sierpiński number by showing that all numbers of the form $78557 \cdot 2^n + 1$ have a factor in the covering set ${3, 5, 7, 13, 19, 37, 73}$.


@[category research solved, AMS 11]
theorem selfridge_78557 : Nat.IsSierpinskiNumber 78557 := by⊢ Nat.IsSierpinskiNumber 78557
  refine ⟨by⊢ ¬2 ∣ 78557 decideAll goals completed! 🐙, fun n => ⟨?_, ?_⟩⟩
  ·refine_1n:ℕ⊢ 1 < 78557 * 2 ^ n + 1 have h : 1 ≤ 2 ^ n := Nat.one_le_pow n 2 (byn:ℕ⊢ 0 < 2refine_1n:ℕh:1 ≤ 2 ^ n⊢ 1 < 78557 * 2 ^ n + 1 norm_numAll goals completed! 🐙refine_1n:ℕh:1 ≤ 2 ^ n⊢ 1 < 78557 * 2 ^ n + 1)refine_1n:ℕh:1 ≤ 2 ^ n⊢ 1 < 78557 * 2 ^ n + 1
    nlinarith [h]All goals completed! 🐙
  ·refine_2n:ℕ⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) have hcov : ∃ p ∈ ([3,5,7,13,19,37,73] : List ℕ), p ∣ (78557 * 2 ^ n + 1) := by⊢ Nat.IsSierpinskiNumber 78557refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      have base : ∀ r, r < 36 → ∃ p ∈ ([3,5,7,13,19,37,73] : List ℕ),
          p ∣ (78557 * 2 ^ r + 1) := by⊢ Nat.IsSierpinskiNumber 78557n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) native_deciden:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      obtain ⟨p, hpmem, hpdvd⟩ := base (n % 36) (Nat.mod_lt _ (byn:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1⊢ 0 < 36n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) norm_numAll goals completed! 🐙n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)))n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1⊢ ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      refine ⟨p, hpmem, ?_⟩n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      have hp36 : (2 : ℕ) ^ 36 ≡ 1 [MOD p] := by⊢ Nat.IsSierpinskiNumber 78557n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) fin_cases hpmem«0»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:3 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 3]«1»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:5 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 5]«2»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:7 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 7]«3»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:13 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 13]«4»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:19 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 19]«5»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:37 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 37]«6»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:73 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 73]n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) <;>«0»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:3 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 3]«1»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:5 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 5]«2»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:7 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 7]«3»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:13 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 13]«4»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:19 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 19]«5»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:37 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 37]«6»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1hpdvd:73 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 73]n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) native_deciden:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      have e2 : (2 : ℕ) ^ n ≡ 2 ^ (n % 36) [MOD p] := by⊢ Nat.IsSierpinskiNumber 78557n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
        conv_lhs => rw [← Nat.div_add_mod n 36, pow_add, pow_mul]n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]| (2 ^ 36) ^ (n / 36) * 2 ^ (n % 36)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
        calc ((2 : ℕ) ^ 36) ^ (n / 36) * 2 ^ (n % 36)
            ≡ 1 ^ (n / 36) * 2 ^ (n % 36) [MOD p] := Nat.ModEq.mul_right _ (hp36.pow _)
          _ = 2 ^ (n % 36) := byn:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ 1 ^ (n / 36) * 2 ^ (n % 36) = 2 ^ (n % 36)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) rw [one_pow,n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ 1 * 2 ^ (n % 36) = 2 ^ (n % 36)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1) one_muln:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]⊢ 2 ^ (n % 36) = 2 ^ (n % 36)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)]n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      have e3 : 78557 * 2 ^ n + 1 ≡ 78557 * 2 ^ (n % 36) + 1 [MOD p] :=
        (e2.mul_left 78557).add_right 1n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p]e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p]e3:78557 * 2 ^ n + 1 ≡ 78557 * 2 ^ (n % 36) + 1 [MOD p]⊢ p ∣ 78557 * 2 ^ n + 1refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
      exact (Nat.modEq_zero_iff_dvd).mp
        (e3.trans ((Nat.modEq_zero_iff_dvd).mpr hpdvd))refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)refine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1⊢ ¬Nat.Prime (78557 * 2 ^ n + 1)
    intro hprimerefine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1hprime:Nat.Prime (78557 * 2 ^ n + 1)⊢ False
    obtain ⟨p, hpmem, hpdvd⟩ := hcovrefine_2n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ n + 1⊢ False
    rcases hprime.eq_one_or_self_of_dvd p hpdvd with h | hrefine_2.inln:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ n + 1h:p = 1⊢ Falserefine_2.inrn:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ n + 1h:p = 78557 * 2 ^ n + 1⊢ False <;>refine_2.inln:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ n + 1h:p = 1⊢ Falserefine_2.inrn:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ n + 1h:p = 78557 * 2 ^ n + 1⊢ False fin_cases hpmemrefine_2.inr.«0»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:3 ∣ 78557 * 2 ^ n + 1h:3 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«1»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:5 ∣ 78557 * 2 ^ n + 1h:5 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«2»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:7 ∣ 78557 * 2 ^ n + 1h:7 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«3»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:13 ∣ 78557 * 2 ^ n + 1h:13 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«4»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:19 ∣ 78557 * 2 ^ n + 1h:19 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«5»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:37 ∣ 78557 * 2 ^ n + 1h:37 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«6»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:73 ∣ 78557 * 2 ^ n + 1h:73 = 78557 * 2 ^ n + 1⊢ False <;>refine_2.inl.«0»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:3 ∣ 78557 * 2 ^ n + 1h:3 = 1⊢ Falserefine_2.inl.«1»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:5 ∣ 78557 * 2 ^ n + 1h:5 = 1⊢ Falserefine_2.inl.«2»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:7 ∣ 78557 * 2 ^ n + 1h:7 = 1⊢ Falserefine_2.inl.«3»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:13 ∣ 78557 * 2 ^ n + 1h:13 = 1⊢ Falserefine_2.inl.«4»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:19 ∣ 78557 * 2 ^ n + 1h:19 = 1⊢ Falserefine_2.inl.«5»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:37 ∣ 78557 * 2 ^ n + 1h:37 = 1⊢ Falserefine_2.inl.«6»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:73 ∣ 78557 * 2 ^ n + 1h:73 = 1⊢ Falserefine_2.inr.«0»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:3 ∣ 78557 * 2 ^ n + 1h:3 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«1»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:5 ∣ 78557 * 2 ^ n + 1h:5 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«2»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:7 ∣ 78557 * 2 ^ n + 1h:7 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«3»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:13 ∣ 78557 * 2 ^ n + 1h:13 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«4»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:19 ∣ 78557 * 2 ^ n + 1h:19 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«5»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:37 ∣ 78557 * 2 ^ n + 1h:37 = 78557 * 2 ^ n + 1⊢ Falserefine_2.inr.«6»n:ℕhprime:Nat.Prime (78557 * 2 ^ n + 1)hpdvd:73 ∣ 78557 * 2 ^ n + 1h:73 = 78557 * 2 ^ n + 1⊢ False omegaAll goals completed! 🐙

The Sierpiński problem (Selfridge's conjecture). Is 78557 the smallest Sierpiński number?

Selfridge conjectured that 78557 is the smallest Sierpiński number. He proved in 1962 that 78557 is indeed a Sierpiński number by showing that all numbers of the form $78557 \cdot 2^n + 1$ have a factor in the covering set ${3, 5, 7, 13, 19, 37, 73}$.

@[category research open, AMS 11]
theorem selfridge_conjecture :
    answer(sorry) ↔ IsLeast {k | k.IsSierpinskiNumber} 78557 := by⊢ True ↔ IsLeast {k | k.IsSierpinskiNumber} 78557
  sorryAll goals completed! 🐙

The prime Sierpiński problem. Is 271129 the smallest prime Sierpiński number?

In 1976, Nathan Mendelsohn determined that the second provable Sierpiński number is the prime $k = 271129$.

@[category research open, AMS 11]
theorem prime_sierpinski_problem :
    answer(sorry) ↔ IsLeast {k | k.IsSierpinskiNumber ∧ k.Prime} 271129 := by⊢ True ↔ IsLeast {k | k.IsSierpinskiNumber ∧ Nat.Prime k} 271129
  sorryAll goals completed! 🐙

The extended Sierpiński problem. Is 271129 the second-smallest Sierpiński number?

Even if 78557 is confirmed as the smallest Sierpiński number, there could exist a composite Sierpiński number $k$ with $78557 < k < 271129$. We formalize "second-smallest" as: the least Sierpiński number $k$ such that there exists exactly one Sierpiński number below it.

@[category research open, AMS 11]
theorem extended_sierpinski_problem :
    answer(sorry) ↔
      IsLeast {k | k.IsSierpinskiNumber ∧
        ∃ k', k'.IsSierpinskiNumber ∧ k' < k} 271129 := by⊢ True ↔ IsLeast {k | k.IsSierpinskiNumber ∧ ∃ k', k'.IsSierpinskiNumber ∧ k' < k} 271129
  sorryAll goals completed! 🐙

end SierpinskiNumber