Wieferich primes

The question

infinite_isWieferichPrime. There are infinitely many Wieferich primes.

isWieferichPrime_iff. Are $1093$ and $3511$ the only Wieferich primes? They are the only known ones: PrimeGrid's search, completed in 2022, shows that any other Wieferich prime exceeds $2^{64}$. On the other hand, the heuristic count of $\log \log x$ Wieferich primes up to $x$ predicts that there are infinitely many, see infinite_isWieferichPrime.

infinite_isWieferichPrimeBase. For any given integer $a>0$, are there infinitely many primes $p$ such that $a^{p-1}\equiv 1(\mathrm{mod}{p}^2)$? The case $a=1$ is trivial, since every prime qualifies (isWieferichPrimeBase_one_iff). So is the case $a=0$ under our definition (isWieferichPrimeBase_zero_iff), which is why the source's restriction to $a>0$ is dropped.

exists_isWieferichPrimeBase_47. Are there any Wieferich primes to base $47$? None is currently known.

A Wieferich prime is a prime $p$ with $2^{p-1}\equiv 1(\mathrm{mod}{p}^2)$. The only known examples are $1093$ and $3511$. It is conjectured that there are infinitely many Wieferich primes; a heuristic argument suggests that the number of Wieferich primes up to $x$ grows like $\log \log x$.

More generally, a prime $p$ is a Wieferich prime to base $a$ if $a^{p-1}\equiv 1(\mathrm{mod}{p}^2)$. Wikipedia's list of unsolved problems also asks whether there are infinitely many Wieferich primes to every base $a>0$, and whether there is any Wieferich prime to base $47$. It is also not known whether there is any Wieferich prime besides $1093$ and $3511$.

Formal statement (Lean 4)

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

theorem infinite_isWieferichPrime : {p : ℕ | IsWieferichPrime p}.Infinite

theorem isWieferichPrime_iff :
    answer(sorry) ↔ ∀ p, IsWieferichPrime p ↔ p = 1093 ∨ p = 3511

theorem infinite_isWieferichPrimeBase :
    answer(sorry) ↔ ∀ a : ℕ, {p : ℕ | IsWieferichPrimeBase a p}.Infinite

theorem exists_isWieferichPrimeBase_47 : answer(sorry) ↔ ∃ p, IsWieferichPrimeBase 47 p

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, List of unsolved problems in mathematics
• Wikipedia, Wieferich prime
• OEIS A001220
• P. Ribenboim, Die Welt der Primzahlen, 2nd ed., Springer (2006), pp. 242–243.
• PrimeGrid, Wieferich and Wall–Sun–Sun Prime Search

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.