Sierpiński number

The question

selfridge_conjecture. 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\}$.

prime_sierpinski_problem. 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$.

extended_sierpinski_problem. 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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.SierpinskiNumber (3 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem selfridge_conjecture :
    answer(sorry) ↔ IsLeast {k | k.IsSierpinskiNumber} 78557

theorem prime_sierpinski_problem :
    answer(sorry) ↔ IsLeast {k | k.IsSierpinskiNumber ∧ k.Prime} 271129

theorem extended_sierpinski_problem :
    answer(sorry) ↔
      IsLeast {k | k.IsSierpinskiNumber ∧
        ∃ k', k'.IsSierpinskiNumber ∧ k' < k} 271129

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

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?

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.