Wikipedia · textbook · AMS 11
mediumknown result, no worker yet
Infinitude of Pell number primes
Theorem · pellNumber_sq_add_pellNumber_succ_sq
Similar to Fibonacci numbers, there exist numerous identities around Pell numbers, i.e. P_{2n+1} = P_n ^ 2 + P_{n+1} ^ 2
Formal statement · Lean 4.lean
theorem pellNumber_sq_add_pellNumber_succ_sq (n : ℕ) :
pellNumber (2 * n + 1) = pellNumber n ^ 2 + pellNumber (n + 1) ^ 2 := by
sorryProof. sorry
Nobody has tried yet.