/-
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 FormalConjecturesUtilInfinitude 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.
namespace PellNumbersThe Pell numbers $P_n$ are defined by $P_0 = 0$, $P_1 = 1$, $P_{n+2} = 2*P_{n+1} + P_n$
def pellNumber : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 1 + 1 => 2 * pellNumber (n + 1) + pellNumber n@[category test, AMS 11]
theorem pellNumber_zero : pellNumber 0 = 0 := rfl@[category test, AMS 11]
theorem pellNumber_one : pellNumber 1 = 1 := rfl@[category test, AMS 11]
theorem pellNumber_two : pellNumber 2 = 2 := rfl@[category test, AMS 11]
theorem pellNumber_five : pellNumber 5 = 29 := rflSimilar to Fibonacci numbers, there exist numerous identities around Pell numbers, i.e. P_{2n+1} = P_n ^ 2 + P_{n+1} ^ 2
n:ℕk:ℕhA:pellNumber (2 * k + 1) = pellNumber k ^ 2 + pellNumber (k + 1) ^ 2hB:pellNumber (2 * k + 2) = 2 * pellNumber (k + 1) * (pellNumber k + pellNumber (k + 1))hstep1:pellNumber (2 * (k + 1) + 1) = 2 * pellNumber (2 * k + 2) + pellNumber (2 * k + 1)hstep2:pellNumber (2 * (k + 1) + 2) = 2 * pellNumber (2 * (k + 1) + 1) + pellNumber (2 * k + 2)hk2:pellNumber (k + 2) = 2 * pellNumber (k + 1) + pellNumber khA':pellNumber (2 * (k + 1) + 1) = pellNumber (k + 1) ^ 2 + pellNumber (k + 2) ^ 2⊢ 2 * (pellNumber (k + 1) ^ 2 + (2 * pellNumber (k + 1) + pellNumber k) ^ 2) +
2 * pellNumber (k + 1) * (pellNumber k + pellNumber (k + 1)) =
2 * (2 * pellNumber (k + 1) + pellNumber k) * (pellNumber (k + 1) + (2 * pellNumber (k + 1) + pellNumber k)); All goals completed! 🐙An explicit formula for Pell numbers, similar to Binet's formula
α:ℝ := 1 + √2hα_def:α = 1 + √2β:ℝ := 1 - √2hβ_def:β = 1 - √2hsq2:√2 ^ 2 = 2hα_sq:α ^ 2 = 2 * α + 1hβ_sq:β ^ 2 = 2 * β + 1h2sq2_ne:2 * √2 ≠ 0hα_rec:∀ (n : ℕ), α ^ (n + 2) = 2 * α ^ (n + 1) + α ^ nhβ_rec:∀ (n : ℕ), β ^ (n + 2) = 2 * β ^ (n + 1) + β ^ nk:ℕhk:↑(pellNumber k) = (α ^ k - β ^ k) / (2 * √2)hk1:↑(pellNumber (k + 1)) = (α ^ (k + 1) - β ^ (k + 1)) / (2 * √2)hrec:pellNumber (k + 1 + 1) = 2 * pellNumber (k + 1) + pellNumber k⊢ 2 * ((α ^ (k + 1) - β ^ (k + 1)) / (2 * √2)) + (α ^ k - β ^ k) / (2 * √2) =
(2 * α ^ (k + 1) + α ^ k - (2 * β ^ (k + 1) + β ^ k)) / (2 * √2)
α:ℝ := 1 + √2hα_def:α = 1 + √2β:ℝ := 1 - √2hβ_def:β = 1 - √2hsq2:√2 ^ 2 = 2hα_sq:α ^ 2 = 2 * α + 1hβ_sq:β ^ 2 = 2 * β + 1h2sq2_ne:2 * √2 ≠ 0hα_rec:∀ (n : ℕ), α ^ (n + 2) = 2 * α ^ (n + 1) + α ^ nhβ_rec:∀ (n : ℕ), β ^ (n + 2) = 2 * β ^ (n + 1) + β ^ nk:ℕhk:↑(pellNumber k) = (α ^ k - β ^ k) / (2 * √2)hk1:↑(pellNumber (k + 1)) = (α ^ (k + 1) - β ^ (k + 1)) / (2 * √2)hrec:pellNumber (k + 1 + 1) = 2 * pellNumber (k + 1) + pellNumber k⊢ 2 * (α ^ (k + 1) - β ^ (k + 1)) + (α ^ k - β ^ k) = 2 * α ^ (k + 1) + α ^ k - (2 * β ^ (k + 1) + β ^ k)
All goals completed! 🐙There are infinitely many prime Pell numbers
@[category research open, AMS 11]
theorem infinite_pellNumber_primes : Infinite {n : ℕ | Prime (pellNumber n)} := ⊢ Infinite ↑{n | Prime (pellNumber n)}
All goals completed! 🐙-- TODO : Formalise connection between Pell numbers and Pell equation x^2 - 2*y^2 = -1
end PellNumbers