Documentation

FormalConjectures.Wikipedia.Pell

Infinitude of Pell number primes #

References:

The Pell numbers $P_n$ are defined by $P_0 = 0$, $P_1 = 1$, $P_{n+2} = 2*P_{n+1} + P_n$. OEIS A129

The conjecture says that there are infinitely many prime Pell numbers.

source
def PellNumbers.pellNumber :
ℕ → ℕ

The Pell numbers $P_n$ are defined by $P_0 = 0$, $P_1 = 1$, $P_{n+2} = 2*P_{n+1} + P_n$

Equations
Instances For
    source
    theorem PellNumbers.pellNumber_zero :
    pellNumber 0 = 0
    source
    theorem PellNumbers.pellNumber_one :
    pellNumber 1 = 1
    source
    theorem PellNumbers.pellNumber_two :
    pellNumber 2 = 2
    source
    theorem PellNumbers.pellNumber_five :
    pellNumber 5 = 29
    source
    theorem PellNumbers.pellNumber_sq_add_pellNumber_succ_sq (n : ℕ) :
    pellNumber (2 * n + 1) = pellNumber n ^ 2 + pellNumber (n + 1) ^ 2

    Similar to Fibonacci numbers, there exist numerous identites around Pell numbers, i.e. P_{2n+1} = P_n ^ 2 + P_{n+1} ^ 2

    source
    theorem PellNumbers.coe_pellNumber_eq (n : ℕ) :
    ↑(pellNumber n) = ((1 + √2) ^ n - (1 - √2) ^ n) / (2 * √2)

    An explicit formula for Pell numbers, similar to Binet's formula

    source
    theorem PellNumbers.infinite_pellNumber_primes :
    Infinite ↑{n : ℕ | Prime (pellNumber n)}

    There are infinitely many prime Pell numbers