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 < 2 norm_numAll goals completed! 🐙)
    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 78557
      have base : ∀ r, r < 36 → ∃ p ∈ ([3,5,7,13,19,37,73] : List ℕ),
          p ∣ (78557 * 2 ^ r + 1) := by⊢ Nat.IsSierpinskiNumber 78557 native_decideAll goals completed! 🐙
      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 := selfridge_78557._proof_1⊢ 0 < 36 norm_numAll goals completed! 🐙))
      refine ⟨p, hpmem, ?_⟩n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1 := selfridge_78557._proof_1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1⊢ p ∣ 78557 * 2 ^ n + 1
      have hp36 : (2 : ℕ) ^ 36 ≡ 1 [MOD p] := by⊢ Nat.IsSierpinskiNumber 78557 fin_cases hpmem«0»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_1hpdvd:73 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 73] <;>«0»n:ℕbase:∀ r < 36, ∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ r + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_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 + 1 := selfridge_78557._proof_1hpdvd:73 ∣ 78557 * 2 ^ (n % 36) + 1⊢ 2 ^ 36 ≡ 1 [MOD 73] native_decideAll goals completed! 🐙
      have e2 : (2 : ℕ) ^ n ≡ 2 ^ (n % 36) [MOD p] := by⊢ Nat.IsSierpinskiNumber 78557
        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 + 1 := selfridge_78557._proof_1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p] := 
  List.Mem.casesOn (motive := fun a x => [3, 5, 7, 13, 19, 37, 73] = a → hpmem ≍ x → 2 ^ 36 ≡ 1 [MOD p]) hpmem
    (fun as h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun p =>
          ∀ (hpmem : p ∈ [3, 5, 7, 13, 19, 37, 73]),
            p ∣ 78557 * 2 ^ (n % 36) + 1 → [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
          (fun hpmem hpdvd tail_eq =>
            Eq.ndrec (motive := fun as => hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 3])
              (fun h => selfridge_78557._proof_2) (eq_of_heq tail_eq))
          (eq_of_heq head_eq) hpmem hpdvd)
    (fun b {as} a h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun b => [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
          (fun tail_eq =>
            Eq.ndrec (motive := fun {as} => ∀ (a : List.Mem p as), hpmem ≍ List.Mem.tail 3 a → 2 ^ 36 ≡ 1 [MOD p])
              (fun a h =>
                List.Mem.casesOn (motive := fun a_1 x => [5, 7, 13, 19, 37, 73] = a_1 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                  (fun as h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun p =>
                        p ∣ 78557 * 2 ^ (n % 36) + 1 →
                          ∀ (a : List.Mem p [5, 7, 13, 19, 37, 73]),
                            [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                        (fun hpdvd a tail_eq =>
                          Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 5])
                            (fun h => selfridge_78557._proof_3) (eq_of_heq tail_eq))
                        (eq_of_heq head_eq) hpdvd a)
                  (fun b {as} a_1 h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun b =>
                        [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_1 → 2 ^ 36 ≡ 1 [MOD p])
                        (fun tail_eq =>
                          Eq.ndrec (motive := fun {as} =>
                            ∀ (a_2 : List.Mem p as), a ≍ List.Mem.tail 5 a_2 → 2 ^ 36 ≡ 1 [MOD p])
                            (fun a_2 h =>
                              List.Mem.casesOn (motive := fun a x =>
                                [7, 13, 19, 37, 73] = a → a_2 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_2
                                (fun as h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun p =>
                                      p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                        ∀ (a : List.Mem p [7, 13, 19, 37, 73]),
                                          [13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun hpdvd a tail_eq =>
                                        Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 7])
                                          (fun h => selfridge_78557._proof_4) (eq_of_heq tail_eq))
                                      (eq_of_heq head_eq) hpdvd a_2)
                                (fun b {as} a h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun b =>
                                      [13, 19, 37, 73] ≍ as → a_2 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun tail_eq =>
                                        Eq.ndrec (motive := fun {as} =>
                                          ∀ (a : List.Mem p as), a_2 ≍ List.Mem.tail 7 a → 2 ^ 36 ≡ 1 [MOD p])
                                          (fun a h =>
                                            List.Mem.casesOn (motive := fun a_3 x =>
                                              [13, 19, 37, 73] = a_3 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                              (fun as h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun p =>
                                                    p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                      ∀ (a : List.Mem p [13, 19, 37, 73]),
                                                        [19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun hpdvd a tail_eq =>
                                                      Eq.ndrec (motive := fun as =>
                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 13])
                                                        (fun h => selfridge_78557._proof_5) (eq_of_heq tail_eq))
                                                    (eq_of_heq head_eq) hpdvd a)
                                              (fun b {as} a_3 h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun b =>
                                                    [19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_3 → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun tail_eq =>
                                                      Eq.ndrec (motive := fun {as} =>
                                                        ∀ (a_4 : List.Mem p as),
                                                          a ≍ List.Mem.tail 13 a_4 → 2 ^ 36 ≡ 1 [MOD p])
                                                        (fun a_4 h =>
                                                          List.Mem.casesOn (motive := fun a x =>
                                                            [19, 37, 73] = a → a_4 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_4
                                                            (fun as h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun p =>
                                                                  p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                    ∀ (a : List.Mem p [19, 37, 73]),
                                                                      [37, 73] ≍ as →
                                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun hpdvd a tail_eq =>
                                                                    Eq.ndrec (motive := fun as =>
                                                                      a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 19])
                                                                      (fun h => selfridge_78557._proof_6)
                                                                      (eq_of_heq tail_eq))
                                                                  (eq_of_heq head_eq) hpdvd a_4)
                                                            (fun b {as} a h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun b =>
                                                                  [37, 73] ≍ as →
                                                                    a_4 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun tail_eq =>
                                                                    Eq.ndrec (motive := fun {as} =>
                                                                      ∀ (a : List.Mem p as),
                                                                        a_4 ≍ List.Mem.tail 19 a → 2 ^ 36 ≡ 1 [MOD p])
                                                                      (fun a h =>
                                                                        List.Mem.casesOn (motive := fun a_5 x =>
                                                                          [37, 73] = a_5 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                                                          (fun as h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun p =>
                                                                                p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                                  ∀ (a : List.Mem p [37, 73]),
                                                                                    [73] ≍ as →
                                                                                      a ≍ List.Mem.head as →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun hpdvd a tail_eq =>
                                                                                  Eq.ndrec (motive := fun as =>
                                                                                    a ≍ List.Mem.head as →
                                                                                      2 ^ 36 ≡ 1 [MOD 37])
                                                                                    (fun h => selfridge_78557._proof_7)
                                                                                    (eq_of_heq tail_eq))
                                                                                (eq_of_heq head_eq) hpdvd a)
                                                                          (fun b {as} a_5 h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun b =>
                                                                                [73] ≍ as →
                                                                                  a ≍ List.Mem.tail b a_5 →
                                                                                    2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun tail_eq =>
                                                                                  Eq.ndrec (motive := fun {as} =>
                                                                                    ∀ (a_6 : List.Mem p as),
                                                                                      a ≍ List.Mem.tail 37 a_6 →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                    (fun a_6 h =>
                                                                                      List.Mem.casesOn (motive :=
                                                                                        fun a x =>
                                                                                        [73] = a →
                                                                                          a_6 ≍ x → 2 ^ 36 ≡ 1 [MOD p])
                                                                                        a_6
                                                                                        (fun as h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (fun b {as} a h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (Eq.refl [73]) (HEq.refl a_6))
                                                                                    (eq_of_heq tail_eq) a_5)
                                                                                (eq_of_heq head_eq))
                                                                          (Eq.refl [37, 73]) (HEq.refl a))
                                                                      (eq_of_heq tail_eq) a)
                                                                  (eq_of_heq head_eq))
                                                            (Eq.refl [19, 37, 73]) (HEq.refl a_4))
                                                        (eq_of_heq tail_eq) a_3)
                                                    (eq_of_heq head_eq))
                                              (Eq.refl [13, 19, 37, 73]) (HEq.refl a))
                                          (eq_of_heq tail_eq) a)
                                      (eq_of_heq head_eq))
                                (Eq.refl [7, 13, 19, 37, 73]) (HEq.refl a_2))
                            (eq_of_heq tail_eq) a_1)
                        (eq_of_heq head_eq))
                  (Eq.refl [5, 7, 13, 19, 37, 73]) (HEq.refl a))
              (eq_of_heq tail_eq) a)
          (eq_of_heq head_eq))
    (Eq.refl [3, 5, 7, 13, 19, 37, 73]) (HEq.refl hpmem)| (2 ^ 36) ^ (n / 36) * 2 ^ (n % 36)
        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 + 1 := selfridge_78557._proof_1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p] := 
  List.Mem.casesOn (motive := fun a x => [3, 5, 7, 13, 19, 37, 73] = a → hpmem ≍ x → 2 ^ 36 ≡ 1 [MOD p]) hpmem
    (fun as h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun p =>
          ∀ (hpmem : p ∈ [3, 5, 7, 13, 19, 37, 73]),
            p ∣ 78557 * 2 ^ (n % 36) + 1 → [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
          (fun hpmem hpdvd tail_eq =>
            Eq.ndrec (motive := fun as => hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 3])
              (fun h => selfridge_78557._proof_2) (eq_of_heq tail_eq))
          (eq_of_heq head_eq) hpmem hpdvd)
    (fun b {as} a h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun b => [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
          (fun tail_eq =>
            Eq.ndrec (motive := fun {as} => ∀ (a : List.Mem p as), hpmem ≍ List.Mem.tail 3 a → 2 ^ 36 ≡ 1 [MOD p])
              (fun a h =>
                List.Mem.casesOn (motive := fun a_1 x => [5, 7, 13, 19, 37, 73] = a_1 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                  (fun as h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun p =>
                        p ∣ 78557 * 2 ^ (n % 36) + 1 →
                          ∀ (a : List.Mem p [5, 7, 13, 19, 37, 73]),
                            [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                        (fun hpdvd a tail_eq =>
                          Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 5])
                            (fun h => selfridge_78557._proof_3) (eq_of_heq tail_eq))
                        (eq_of_heq head_eq) hpdvd a)
                  (fun b {as} a_1 h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun b =>
                        [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_1 → 2 ^ 36 ≡ 1 [MOD p])
                        (fun tail_eq =>
                          Eq.ndrec (motive := fun {as} =>
                            ∀ (a_2 : List.Mem p as), a ≍ List.Mem.tail 5 a_2 → 2 ^ 36 ≡ 1 [MOD p])
                            (fun a_2 h =>
                              List.Mem.casesOn (motive := fun a x =>
                                [7, 13, 19, 37, 73] = a → a_2 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_2
                                (fun as h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun p =>
                                      p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                        ∀ (a : List.Mem p [7, 13, 19, 37, 73]),
                                          [13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun hpdvd a tail_eq =>
                                        Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 7])
                                          (fun h => selfridge_78557._proof_4) (eq_of_heq tail_eq))
                                      (eq_of_heq head_eq) hpdvd a_2)
                                (fun b {as} a h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun b =>
                                      [13, 19, 37, 73] ≍ as → a_2 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun tail_eq =>
                                        Eq.ndrec (motive := fun {as} =>
                                          ∀ (a : List.Mem p as), a_2 ≍ List.Mem.tail 7 a → 2 ^ 36 ≡ 1 [MOD p])
                                          (fun a h =>
                                            List.Mem.casesOn (motive := fun a_3 x =>
                                              [13, 19, 37, 73] = a_3 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                              (fun as h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun p =>
                                                    p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                      ∀ (a : List.Mem p [13, 19, 37, 73]),
                                                        [19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun hpdvd a tail_eq =>
                                                      Eq.ndrec (motive := fun as =>
                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 13])
                                                        (fun h => selfridge_78557._proof_5) (eq_of_heq tail_eq))
                                                    (eq_of_heq head_eq) hpdvd a)
                                              (fun b {as} a_3 h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun b =>
                                                    [19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_3 → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun tail_eq =>
                                                      Eq.ndrec (motive := fun {as} =>
                                                        ∀ (a_4 : List.Mem p as),
                                                          a ≍ List.Mem.tail 13 a_4 → 2 ^ 36 ≡ 1 [MOD p])
                                                        (fun a_4 h =>
                                                          List.Mem.casesOn (motive := fun a x =>
                                                            [19, 37, 73] = a → a_4 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_4
                                                            (fun as h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun p =>
                                                                  p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                    ∀ (a : List.Mem p [19, 37, 73]),
                                                                      [37, 73] ≍ as →
                                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun hpdvd a tail_eq =>
                                                                    Eq.ndrec (motive := fun as =>
                                                                      a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 19])
                                                                      (fun h => selfridge_78557._proof_6)
                                                                      (eq_of_heq tail_eq))
                                                                  (eq_of_heq head_eq) hpdvd a_4)
                                                            (fun b {as} a h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun b =>
                                                                  [37, 73] ≍ as →
                                                                    a_4 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun tail_eq =>
                                                                    Eq.ndrec (motive := fun {as} =>
                                                                      ∀ (a : List.Mem p as),
                                                                        a_4 ≍ List.Mem.tail 19 a → 2 ^ 36 ≡ 1 [MOD p])
                                                                      (fun a h =>
                                                                        List.Mem.casesOn (motive := fun a_5 x =>
                                                                          [37, 73] = a_5 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                                                          (fun as h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun p =>
                                                                                p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                                  ∀ (a : List.Mem p [37, 73]),
                                                                                    [73] ≍ as →
                                                                                      a ≍ List.Mem.head as →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun hpdvd a tail_eq =>
                                                                                  Eq.ndrec (motive := fun as =>
                                                                                    a ≍ List.Mem.head as →
                                                                                      2 ^ 36 ≡ 1 [MOD 37])
                                                                                    (fun h => selfridge_78557._proof_7)
                                                                                    (eq_of_heq tail_eq))
                                                                                (eq_of_heq head_eq) hpdvd a)
                                                                          (fun b {as} a_5 h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun b =>
                                                                                [73] ≍ as →
                                                                                  a ≍ List.Mem.tail b a_5 →
                                                                                    2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun tail_eq =>
                                                                                  Eq.ndrec (motive := fun {as} =>
                                                                                    ∀ (a_6 : List.Mem p as),
                                                                                      a ≍ List.Mem.tail 37 a_6 →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                    (fun a_6 h =>
                                                                                      List.Mem.casesOn (motive :=
                                                                                        fun a x =>
                                                                                        [73] = a →
                                                                                          a_6 ≍ x → 2 ^ 36 ≡ 1 [MOD p])
                                                                                        a_6
                                                                                        (fun as h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (fun b {as} a h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (Eq.refl [73]) (HEq.refl a_6))
                                                                                    (eq_of_heq tail_eq) a_5)
                                                                                (eq_of_heq head_eq))
                                                                          (Eq.refl [37, 73]) (HEq.refl a))
                                                                      (eq_of_heq tail_eq) a)
                                                                  (eq_of_heq head_eq))
                                                            (Eq.refl [19, 37, 73]) (HEq.refl a_4))
                                                        (eq_of_heq tail_eq) a_3)
                                                    (eq_of_heq head_eq))
                                              (Eq.refl [13, 19, 37, 73]) (HEq.refl a))
                                          (eq_of_heq tail_eq) a)
                                      (eq_of_heq head_eq))
                                (Eq.refl [7, 13, 19, 37, 73]) (HEq.refl a_2))
                            (eq_of_heq tail_eq) a_1)
                        (eq_of_heq head_eq))
                  (Eq.refl [5, 7, 13, 19, 37, 73]) (HEq.refl a))
              (eq_of_heq tail_eq) a)
          (eq_of_heq head_eq))
    (Eq.refl [3, 5, 7, 13, 19, 37, 73]) (HEq.refl hpmem)⊢ 1 ^ (n / 36) * 2 ^ (n % 36) = 2 ^ (n % 36) rw [one_pow, one_mul]All goals completed! 🐙
      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 + 1 := selfridge_78557._proof_1p:ℕhpmem:p ∈ [3, 5, 7, 13, 19, 37, 73]hpdvd:p ∣ 78557 * 2 ^ (n % 36) + 1hp36:2 ^ 36 ≡ 1 [MOD p] := 
  List.Mem.casesOn (motive := fun a x => [3, 5, 7, 13, 19, 37, 73] = a → hpmem ≍ x → 2 ^ 36 ≡ 1 [MOD p]) hpmem
    (fun as h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun p =>
          ∀ (hpmem : p ∈ [3, 5, 7, 13, 19, 37, 73]),
            p ∣ 78557 * 2 ^ (n % 36) + 1 → [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
          (fun hpmem hpdvd tail_eq =>
            Eq.ndrec (motive := fun as => hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 3])
              (fun h => selfridge_78557._proof_2) (eq_of_heq tail_eq))
          (eq_of_heq head_eq) hpmem hpdvd)
    (fun b {as} a h =>
      List.cons.noConfusion h fun head_eq =>
        Eq.ndrec (motive := fun b => [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
          (fun tail_eq =>
            Eq.ndrec (motive := fun {as} => ∀ (a : List.Mem p as), hpmem ≍ List.Mem.tail 3 a → 2 ^ 36 ≡ 1 [MOD p])
              (fun a h =>
                List.Mem.casesOn (motive := fun a_1 x => [5, 7, 13, 19, 37, 73] = a_1 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                  (fun as h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun p =>
                        p ∣ 78557 * 2 ^ (n % 36) + 1 →
                          ∀ (a : List.Mem p [5, 7, 13, 19, 37, 73]),
                            [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                        (fun hpdvd a tail_eq =>
                          Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 5])
                            (fun h => selfridge_78557._proof_3) (eq_of_heq tail_eq))
                        (eq_of_heq head_eq) hpdvd a)
                  (fun b {as} a_1 h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun b =>
                        [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_1 → 2 ^ 36 ≡ 1 [MOD p])
                        (fun tail_eq =>
                          Eq.ndrec (motive := fun {as} =>
                            ∀ (a_2 : List.Mem p as), a ≍ List.Mem.tail 5 a_2 → 2 ^ 36 ≡ 1 [MOD p])
                            (fun a_2 h =>
                              List.Mem.casesOn (motive := fun a x =>
                                [7, 13, 19, 37, 73] = a → a_2 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_2
                                (fun as h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun p =>
                                      p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                        ∀ (a : List.Mem p [7, 13, 19, 37, 73]),
                                          [13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun hpdvd a tail_eq =>
                                        Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 7])
                                          (fun h => selfridge_78557._proof_4) (eq_of_heq tail_eq))
                                      (eq_of_heq head_eq) hpdvd a_2)
                                (fun b {as} a h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun b =>
                                      [13, 19, 37, 73] ≍ as → a_2 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun tail_eq =>
                                        Eq.ndrec (motive := fun {as} =>
                                          ∀ (a : List.Mem p as), a_2 ≍ List.Mem.tail 7 a → 2 ^ 36 ≡ 1 [MOD p])
                                          (fun a h =>
                                            List.Mem.casesOn (motive := fun a_3 x =>
                                              [13, 19, 37, 73] = a_3 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                              (fun as h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun p =>
                                                    p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                      ∀ (a : List.Mem p [13, 19, 37, 73]),
                                                        [19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun hpdvd a tail_eq =>
                                                      Eq.ndrec (motive := fun as =>
                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 13])
                                                        (fun h => selfridge_78557._proof_5) (eq_of_heq tail_eq))
                                                    (eq_of_heq head_eq) hpdvd a)
                                              (fun b {as} a_3 h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun b =>
                                                    [19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_3 → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun tail_eq =>
                                                      Eq.ndrec (motive := fun {as} =>
                                                        ∀ (a_4 : List.Mem p as),
                                                          a ≍ List.Mem.tail 13 a_4 → 2 ^ 36 ≡ 1 [MOD p])
                                                        (fun a_4 h =>
                                                          List.Mem.casesOn (motive := fun a x =>
                                                            [19, 37, 73] = a → a_4 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_4
                                                            (fun as h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun p =>
                                                                  p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                    ∀ (a : List.Mem p [19, 37, 73]),
                                                                      [37, 73] ≍ as →
                                                                        a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun hpdvd a tail_eq =>
                                                                    Eq.ndrec (motive := fun as =>
                                                                      a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 19])
                                                                      (fun h => selfridge_78557._proof_6)
                                                                      (eq_of_heq tail_eq))
                                                                  (eq_of_heq head_eq) hpdvd a_4)
                                                            (fun b {as} a h =>
                                                              List.cons.noConfusion h fun head_eq =>
                                                                Eq.ndrec (motive := fun b =>
                                                                  [37, 73] ≍ as →
                                                                    a_4 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun tail_eq =>
                                                                    Eq.ndrec (motive := fun {as} =>
                                                                      ∀ (a : List.Mem p as),
                                                                        a_4 ≍ List.Mem.tail 19 a → 2 ^ 36 ≡ 1 [MOD p])
                                                                      (fun a h =>
                                                                        List.Mem.casesOn (motive := fun a_5 x =>
                                                                          [37, 73] = a_5 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                                                          (fun as h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun p =>
                                                                                p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                                  ∀ (a : List.Mem p [37, 73]),
                                                                                    [73] ≍ as →
                                                                                      a ≍ List.Mem.head as →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun hpdvd a tail_eq =>
                                                                                  Eq.ndrec (motive := fun as =>
                                                                                    a ≍ List.Mem.head as →
                                                                                      2 ^ 36 ≡ 1 [MOD 37])
                                                                                    (fun h => selfridge_78557._proof_7)
                                                                                    (eq_of_heq tail_eq))
                                                                                (eq_of_heq head_eq) hpdvd a)
                                                                          (fun b {as} a_5 h =>
                                                                            List.cons.noConfusion h fun head_eq =>
                                                                              Eq.ndrec (motive := fun b =>
                                                                                [73] ≍ as →
                                                                                  a ≍ List.Mem.tail b a_5 →
                                                                                    2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun tail_eq =>
                                                                                  Eq.ndrec (motive := fun {as} =>
                                                                                    ∀ (a_6 : List.Mem p as),
                                                                                      a ≍ List.Mem.tail 37 a_6 →
                                                                                        2 ^ 36 ≡ 1 [MOD p])
                                                                                    (fun a_6 h =>
                                                                                      List.Mem.casesOn (motive :=
                                                                                        fun a x =>
                                                                                        [73] = a →
                                                                                          a_6 ≍ x → 2 ^ 36 ≡ 1 [MOD p])
                                                                                        a_6
                                                                                        (fun as h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (fun b {as} a h =>
                                                                                          List.cons.noConfusion h ⋯)
                                                                                        (Eq.refl [73]) (HEq.refl a_6))
                                                                                    (eq_of_heq tail_eq) a_5)
                                                                                (eq_of_heq head_eq))
                                                                          (Eq.refl [37, 73]) (HEq.refl a))
                                                                      (eq_of_heq tail_eq) a)
                                                                  (eq_of_heq head_eq))
                                                            (Eq.refl [19, 37, 73]) (HEq.refl a_4))
                                                        (eq_of_heq tail_eq) a_3)
                                                    (eq_of_heq head_eq))
                                              (Eq.refl [13, 19, 37, 73]) (HEq.refl a))
                                          (eq_of_heq tail_eq) a)
                                      (eq_of_heq head_eq))
                                (Eq.refl [7, 13, 19, 37, 73]) (HEq.refl a_2))
                            (eq_of_heq tail_eq) a_1)
                        (eq_of_heq head_eq))
                  (Eq.refl [5, 7, 13, 19, 37, 73]) (HEq.refl a))
              (eq_of_heq tail_eq) a)
          (eq_of_heq head_eq))
    (Eq.refl [3, 5, 7, 13, 19, 37, 73]) (HEq.refl hpmem)e2:2 ^ n ≡ 2 ^ (n % 36) [MOD p] := 
  Eq.mpr
    (id
      ((fun a a_1 e_a =>
          Eq.rec (motive := fun a_2 e_a => ∀ (b : ℕ), (a ≡ b [MOD p]) = (a_2 ≡ b [MOD p]))
            (fun b => Eq.refl (a ≡ b [MOD p])) e_a)
        (2 ^ n) ((2 ^ 36) ^ (n / 36) * 2 ^ (n % 36))
        (Eq.trans (congrArg (fun _a => 2 ^ _a) (Eq.symm (Nat.div_add_mod n 36)))
          (Eq.trans (congrArg (fun _a => _a) (pow_add 2 (36 * (n / 36)) (n % 36)))
            (Eq.trans (congrArg (fun _a => _a * 2 ^ (n % 36)) (pow_mul 2 36 (n / 36)))
              (Eq.refl ((2 ^ 36) ^ (n / 36) * 2 ^ (n % 36))))))
        (2 ^ (n % 36))))
    (Trans.trans (Nat.ModEq.mul_right (2 ^ (n % 36)) (Nat.ModEq.pow (n / 36) hp36))
      (Eq.mpr (id (congrArg (fun _a => _a * 2 ^ (n % 36) = 2 ^ (n % 36)) (one_pow (n / 36))))
        (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (n % 36)) (one_mul (2 ^ (n % 36))))) (Eq.refl (2 ^ (n % 36))))))e3:78557 * 2 ^ n + 1 ≡ 78557 * 2 ^ (n % 36) + 1 [MOD p] := Nat.ModEq.add_right 1 (Nat.ModEq.mul_left 78557 e2)⊢ p ∣ 78557 * 2 ^ n + 1
      exact (Nat.modEq_zero_iff_dvd).mp
        (e3.trans ((Nat.modEq_zero_iff_dvd).mpr hpdvd))All goals completed! 🐙
    intro hprimerefine_2n:ℕhcov:∃ p ∈ [3, 5, 7, 13, 19, 37, 73], p ∣ 78557 * 2 ^ n + 1 := 
  have base := selfridge_78557._proof_1;
  Exists.casesOn
    (base (n % 36)
      (Nat.mod_lt n
        (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0))
          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 36)) (Eq.refl false))))
    fun p h =>
    And.casesOn h fun hpmem hpdvd =>
      Exists.intro p
        ⟨hpmem,
          have hp36 :=
            List.Mem.casesOn (motive := fun a x => [3, 5, 7, 13, 19, 37, 73] = a → hpmem ≍ x → 2 ^ 36 ≡ 1 [MOD p]) hpmem
              (fun as h =>
                List.cons.noConfusion h fun head_eq =>
                  Eq.ndrec (motive := fun p =>
                    ∀ (hpmem : p ∈ [3, 5, 7, 13, 19, 37, 73]),
                      p ∣ 78557 * 2 ^ (n % 36) + 1 →
                        [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                    (fun hpmem hpdvd tail_eq =>
                      Eq.ndrec (motive := fun as => hpmem ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 3])
                        (fun h => selfridge_78557._proof_2) (eq_of_heq tail_eq))
                    (eq_of_heq head_eq) hpmem hpdvd)
              (fun b {as} a h =>
                List.cons.noConfusion h fun head_eq =>
                  Eq.ndrec (motive := fun b =>
                    [5, 7, 13, 19, 37, 73] ≍ as → hpmem ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                    (fun tail_eq =>
                      Eq.ndrec (motive := fun {as} =>
                        ∀ (a : List.Mem p as), hpmem ≍ List.Mem.tail 3 a → 2 ^ 36 ≡ 1 [MOD p])
                        (fun a h =>
                          List.Mem.casesOn (motive := fun a_1 x =>
                            [5, 7, 13, 19, 37, 73] = a_1 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                            (fun as h =>
                              List.cons.noConfusion h fun head_eq =>
                                Eq.ndrec (motive := fun p =>
                                  p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                    ∀ (a : List.Mem p [5, 7, 13, 19, 37, 73]),
                                      [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                  (fun hpdvd a tail_eq =>
                                    Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 5])
                                      (fun h => selfridge_78557._proof_3) (eq_of_heq tail_eq))
                                  (eq_of_heq head_eq) hpdvd a)
                            (fun b {as} a_1 h =>
                              List.cons.noConfusion h fun head_eq =>
                                Eq.ndrec (motive := fun b =>
                                  [7, 13, 19, 37, 73] ≍ as → a ≍ List.Mem.tail b a_1 → 2 ^ 36 ≡ 1 [MOD p])
                                  (fun tail_eq =>
                                    Eq.ndrec (motive := fun {as} =>
                                      ∀ (a_2 : List.Mem p as), a ≍ List.Mem.tail 5 a_2 → 2 ^ 36 ≡ 1 [MOD p])
                                      (fun a_2 h =>
                                        List.Mem.casesOn (motive := fun a x =>
                                          [7, 13, 19, 37, 73] = a → a_2 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_2
                                          (fun as h =>
                                            List.cons.noConfusion h fun head_eq =>
                                              Eq.ndrec (motive := fun p =>
                                                p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                  ∀ (a : List.Mem p [7, 13, 19, 37, 73]),
                                                    [13, 19, 37, 73] ≍ as → a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                (fun hpdvd a tail_eq =>
                                                  Eq.ndrec (motive := fun as => a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 7])
                                                    (fun h => selfridge_78557._proof_4) (eq_of_heq tail_eq))
                                                (eq_of_heq head_eq) hpdvd a_2)
                                          (fun b {as} a h =>
                                            List.cons.noConfusion h fun head_eq =>
                                              Eq.ndrec (motive := fun b =>
                                                [13, 19, 37, 73] ≍ as → a_2 ≍ List.Mem.tail b a → 2 ^ 36 ≡ 1 [MOD p])
                                                (fun tail_eq =>
                                                  Eq.ndrec (motive := fun {as} =>
                                                    ∀ (a : List.Mem p as), a_2 ≍ List.Mem.tail 7 a → 2 ^ 36 ≡ 1 [MOD p])
                                                    (fun a h =>
                                                      List.Mem.casesOn (motive := fun a_3 x =>
                                                        [13, 19, 37, 73] = a_3 → a ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a
                                                        (fun as h =>
                                                          List.cons.noConfusion h fun head_eq =>
                                                            Eq.ndrec (motive := fun p =>
                                                              p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                ∀ (a : List.Mem p [13, 19, 37, 73]),
                                                                  [19, 37, 73] ≍ as →
                                                                    a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD p])
                                                              (fun hpdvd a tail_eq =>
                                                                Eq.ndrec (motive := fun as =>
                                                                  a ≍ List.Mem.head as → 2 ^ 36 ≡ 1 [MOD 13])
                                                                  (fun h => selfridge_78557._proof_5) (eq_of_heq tail_eq))
                                                              (eq_of_heq head_eq) hpdvd a)
                                                        (fun b {as} a_3 h =>
                                                          List.cons.noConfusion h fun head_eq =>
                                                            Eq.ndrec (motive := fun b =>
                                                              [19, 37, 73] ≍ as →
                                                                a ≍ List.Mem.tail b a_3 → 2 ^ 36 ≡ 1 [MOD p])
                                                              (fun tail_eq =>
                                                                Eq.ndrec (motive := fun {as} =>
                                                                  ∀ (a_4 : List.Mem p as),
                                                                    a ≍ List.Mem.tail 13 a_4 → 2 ^ 36 ≡ 1 [MOD p])
                                                                  (fun a_4 h =>
                                                                    List.Mem.casesOn (motive := fun a x =>
                                                                      [19, 37, 73] = a → a_4 ≍ x → 2 ^ 36 ≡ 1 [MOD p]) a_4
                                                                      (fun as h =>
                                                                        List.cons.noConfusion h fun head_eq =>
                                                                          Eq.ndrec (motive := fun p =>
                                                                            p ∣ 78557 * 2 ^ (n % 36) + 1 →
                                                                              ∀ (a : List.Mem p [19, 37, 73]),
                                                                                [37, 73] ≍ as →
                                                                                  a ≍ List.Mem.head as →
                                                                                    2 ^ 36 ≡ 1 [MOD p])
                                                                            (fun hpdvd a tail_eq =>
                                                                              Eq.ndrec (motive := fun as =>
                                                                                a ≍ List.Mem.head as →
                                                                                  2 ^ 36 ≡ 1 [MOD 19])
                                                                                (fun h => selfridge_78557._proof_6)
                                                                                (eq_of_heq tail_eq))
                                                                            (eq_of_heq head_eq) hpdvd a_4)
                                                                      (fun b {as} a h =>
                                                                        List.cons.noConfusion h fun head_eq =>
                                                                          Eq.ndrec (motive := fun b =>
                                                                            [37, 73] ≍ as →
                                                                              a_4 ≍ List.Mem.tail b a →
                                                                                2 ^ 36 ≡ 1 [MOD p])
                                                                            (fun tail_eq =>
                                                                              Eq.ndrec (motive := fun {as} =>
                                                                                ∀ (a : List.Mem p as),
                                                                                  a_4 ≍ List.Mem.tail 19 a →
                                                                                    2 ^ 36 ≡ 1 [MOD p])
                                                                                (fun a h =>
                                                                                  List.Mem.casesOn (motive := fun a_5 x =>
                                                                                    [37, 73] = a_5 → ⋯) a
                                                                                    (fun as h =>
                                                                                      List.cons.noConfusion h ⋯)
                                                                                    (fun b {as} a_5 h =>
                                                                                      List.cons.noConfusion h ⋯)
                                                                                    (Eq.refl [37, 73]) (HEq.refl a))
                                                                                (eq_of_heq tail_eq) a)
                                                                            (eq_of_heq head_eq))
                                                                      (Eq.refl [19, 37, 73]) (HEq.refl a_4))
                                                                  (eq_of_heq tail_eq) a_3)
                                                              (eq_of_heq head_eq))
                                                        (Eq.refl [13, 19, 37, 73]) (HEq.refl a))
                                                    (eq_of_heq tail_eq) a)
                                                (eq_of_heq head_eq))
                                          (Eq.refl [7, 13, 19, 37, 73]) (HEq.refl a_2))
                                      (eq_of_heq tail_eq) a_1)
                                  (eq_of_heq head_eq))
                            (Eq.refl [5, 7, 13, 19, 37, 73]) (HEq.refl a))
                        (eq_of_heq tail_eq) a)
                    (eq_of_heq head_eq))
              (Eq.refl [3, 5, 7, 13, 19, 37, 73]) (HEq.refl hpmem);
          have e2 :=
            Eq.mpr
              (id
                ((fun a a_1 e_a =>
                    Eq.rec (motive := fun a_2 e_a => ∀ (b : ℕ), (a ≡ b [MOD p]) = (a_2 ≡ b [MOD p]))
                      (fun b => Eq.refl (a ≡ b [MOD p])) e_a)
                  (2 ^ n) ((2 ^ 36) ^ (n / 36) * 2 ^ (n % 36))
                  (Eq.trans (congrArg (fun _a => 2 ^ _a) (Eq.symm (Nat.div_add_mod n 36)))
                    (Eq.trans (congrArg (fun _a => _a) (pow_add 2 (36 * (n / 36)) (n % 36)))
                      (Eq.trans (congrArg (fun _a => _a * 2 ^ (n % 36)) (pow_mul 2 36 (n / 36)))
                        (Eq.refl ((2 ^ 36) ^ (n / 36) * 2 ^ (n % 36))))))
                  (2 ^ (n % 36))))
              (Trans.trans (Nat.ModEq.mul_right (2 ^ (n % 36)) (Nat.ModEq.pow (n / 36) hp36))
                (Eq.mpr (id (congrArg (fun _a => _a * 2 ^ (n % 36) = 2 ^ (n % 36)) (one_pow (n / 36))))
                  (Eq.mpr (id (congrArg (fun _a => _a = 2 ^ (n % 36)) (one_mul (2 ^ (n % 36)))))
                    (Eq.refl (2 ^ (n % 36))))));
          have e3 := Nat.ModEq.add_right 1 (Nat.ModEq.mul_left 78557 e2);
          Nat.modEq_zero_iff_dvd.mp (Nat.ModEq.trans e3 (Nat.modEq_zero_iff_dvd.mpr hpdvd))⟩hprime: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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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