Squares in Fibonacci and Lucas sequences

TheoremCohn's theorem on Lucas numbers of the form \(2x^2\)#✓fully proved

Let \(L_n\) denote the Lucas numbers, with \(L_0 = 2\), \(L_1 = 1\) and \(L_{n+2} = L_{n+1} + L_n\). If \(n\) and \(x\) are natural numbers with \(n \ge 1\) and \(L_n = 2x^2\), then \(n = 6\).

This is the fourth claim of Theorem 2.1 of Keskin and Yosma.

theorem cohn_twice_square_lucas (n x : ℕ) (hn : 0 < n)
    (h : lucasNumber n = 2 * x ^ 2) : n = 6

Uses 1 · Used by 2

Statement usesLucas numbers

Used byCohn's theorem on square Fibonacci numbers · Cohn's theorem on Fibonacci numbers of the form \(2x^2\)

TheoremCohn's theorem on square Lucas numbers#✓fully proved

Let \(L_0 = 2\), \(L_1 = 1\) and \(L_{n+2} = L_{n+1} + L_n\) be the Lucas numbers. If \(n \ge 1\) and \(L_n = x^2\) for some natural number \(x\), then \(n = 1\) or \(n = 3\).

This is the third claim of Theorem 2.1 of Keskin and Yosma, which they attribute to Cohn.

theorem cohn_square_lucas (n x : ℕ) (hn : 0 < n)
    (h : lucasNumber n = x ^ 2) : n = 1 ∨ n = 3

Uses 1 · Used by 2

Statement usesLucas numbers

Used byCohn's theorem on square Fibonacci numbers · Cohn's theorem on Fibonacci numbers of the form \(2x^2\)

TheoremCohn's theorem on square Fibonacci numbers#✓fully proved

Let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\). If \(n\) and \(x\) are natural numbers with \(n \ge 1\) and \(F_n = x^2\), then \(n \in \{1, 2, 12\}\).

This is the first claim of Theorem 2.1 of Keskin and Yosma.

theorem cohn_square_fibonacci (n x : ℕ) (hn : 0 < n)
    (h : Nat.fib n = x ^ 2) : n = 1 ∨ n = 2 ∨ n = 12

Uses 3

Proof usesCohn's theorem on square Lucas numbers · Cohn's theorem on Lucas numbers of the form \(2x^2\) · Lucas numbers

TheoremCohn's theorem on Fibonacci numbers of the form \(2x^2\)#✓fully proved

Let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\). If \(n\) and \(x\) are natural numbers with \(n \ge 1\) and \(F_n = 2x^2\), then \(n \in \{3, 6\}\).

This is the second claim of Theorem 2.1 of Keskin and Yosma.

theorem cohn_twice_square_fibonacci (n x : ℕ) (hn : 0 < n)
    (h : Nat.fib n = 2 * x ^ 2) : n = 3 ∨ n = 6

Uses 3

Proof usesCohn's theorem on square Lucas numbers · Cohn's theorem on Lucas numbers of the form \(2x^2\) · Lucas numbers

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.