Documentation

FormalConjectures.Wikipedia.WallSunSun

Infinitude of Wall–Sun–Sun primes #

Reference: Wikipedia

A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number. It is conjectured that there is at least one Wall–Sun–Sun prime.

A prime $p$ is a Wall–Sun–Sun prime if and only if $L_p \equiv 1 \pmod{p^2}$, where $L_p$ is the $p$-th Lucas number. It is conjectured that there are infinitely many Wall-Sun-Sun primes.

theorem infinite_isWallSunSunPrime_of_disc_eq (D : ℕ+) :
{p : | ∃ (a : ) (b : ), a ^ 2 - 4 * b = D IsLucasWieferichPrime a b p}.Infinite

A Lucas–Wieferich prime associated with $(a,b)$ is a prime $p$ such $U_{p-\varepsilon}(a,b) \equiv 0 \pmod{p^2}$ where $U(a,b)$ is the Lucas sequence of the first kind and $\varepsilon$ is the Legendre symbol $\left({\tfrac {a^{2}-4b}{p}}\right)$. The discriminant of this number is the quantity $a^2 - 4b$. It is conjectured that there are infinitely many Lucas–Wieferich primes of any given discriminant.