The only squares in the Fibonacci sequence are 0, 1, and 144. We implemented a proof of this theorem in the Lean Theorem Prover. In this paper, we will discuss our methods as well as some implementation problems we faced and their solutions. Formalization is the process of implementing mathematical statements and their proofs in a theorem prover such as Coq, Lean, Isabelle, etc. These systems verify that every step of a proof is justified by checking a chain of implications down to the axioms. In this paper, we will discuss our novel formalization of the statement that 0,1, and 144 are the only Fibonacci squares in the Lean Theorem Prover. Let N0 be the set of natural numbers including 0. We defined the Fibonacci and Lucas sequences as
: N0 → N0 0 = 0 1 = 1 +2 = +1 + , : N0 → N0 0 = 2 1 = 1 +2 = +1 + .
Theorem 3. Let , ∈ N0 such that = 2. Then = 0, 1, 2, 12.
This was an old conjecture answering a natural question: the characterization of squares
in one of the most extensively studied sequences. We implemented a proof due to Cohn
found in [
Cohn [
Before proving the only Fibonacci squares are 0, 1, and 144, [
Theorem 2. The only numbers in the Lucas sequence that are 2 times a square are 2 and 18.
To prove Theorem 1, we note the following three key lemmas that hold for all integers . (a) 2 = 2 + (− 1)− 1 · 2. (b) +2 ≡ − (mod ) for any even integer not divisible by 3. (c) ≡ 3 (mod 4) for any even integer not divisible by 3.
For odd Lucas terms notice that 1 = 1 is a square. Then consider ≡ 1 (mod 4), ̸= 1. Write = 1 + 2 · 3 · where is an even integer not divisible by 3. By (b), ≡ − 1 (mod ). And by (c), ≡ 3 (mod 4). So if is a square, − 1 is a quadratic residue modulo a number congruent to 3 (mod 4) which is a contradiction. Let us call this argument above the reduction argument. The case for when ≡ 3 (mod 4) is analogous. Lastly, by (a), even Lucas terms cannot be squares.
The proof for Theorem 2 uses essentially the same idea. We look at the the residue class
modulo 8 of the index of a Lucas square. If there are no such indices in some residue class,
then we can prove that half of the Lucas terms under consideration are indeed non-residues by
observing patterns of Lucas numbers modulo 8 (Preliminary 13 of [
Finally, we can prove that the only Fibonacci squares are 0, 1, and 144. Suppose = 2 for some integers and . If ≡ 1 (mod 4) notice that 1 is a square so use the reduction argument to prove impossibility of other squares. If ≡ 3 (mod 4), we are already done since = − thus reducing it to − ≡ 1 (mod 4). If is even, one can prove = /2/2 and also that gcd(/2, /2) ≤ 2. If the product of two numbers is a square then each of them is the gcd of the two numbers times a square. So we resolve two cases based on the possible values of the gcd, and use Theorems 1 and 2 to obtain the result.
These are the 13 preliminary lemmas in [
+1 = +2 + , ++1 = +1+1 + .
+1 > 0 and > 0, gcd(+1, +2) = 1,
Fibonacci residue patterns modulo 2,
Lucas residue patterns moduli 2, 3, and 4.
Additionally we proved some lemmas that shortened our proofs. For example, formalizing ∀, ∈ N0, ≤ or ∃( ∈ N0), = + + 1 helped verify base cases for induction eficiently. Now we shall discuss two problems we faced.
Perhaps, we could have proved some of our identities using the closed form for the Fibonacci or Lucas sequences. However, this was problematic as performing algebraic manipulations in Lean with √5 would not have been easy or eficient. Tactics such as simp and ring are far more efective in manipulating integers.
Hence, we decided to prove all of our identities with induction. This was indeed much easier to implement. For example, proving 2+ = 5 + , for natural numbers, took merely 7 lines with two-step induction.
Lean has a very large library of lemmas and theorems proven for natural numbers. To begin
with, we defined our sequences (both Fibonacci and Lucas) from N0 → N0, although [
However, rather than defining our sequences over integers, we insisted on their natural
number definitions and modified the proof of Theorem 3 slightly. Preliminaries 1, 2, 11 and 12
(from [
Preliminary 2. 2+ = 5 + .
Preliminary 11. +2 ≡ − (mod ).
Preliminary 12. +2 ≡ −
(mod ).
We proved the following facts instead ∀, , ∈ N0, 2 | , 3 ∤ , (1) 2+ = + . (2) 2 = (− 1)+ + (− 1)+1+. (3) 2+ = 5 + . (4) 2 = (− 1)+1 · 5+ + (− 1)+. (5) | +2 + . (6) 2 ≥ =⇒ | 2− + (− 1). (7) | +2 + . (8) 2 ≥ =⇒ | 2− + (− 1)+1.
That is, for preliminaries 1, 2, 11 and 12, we formalized an addition version and a subtraction
version separately. Also, we did not need to formalize preliminaries 8 and 9 of [
Let = 4 · 3 · − 1 for , ∈ N0 and gcd(, 3) = 1. Then, (9) (10) (11) (12) 2 | +4 + , 2 | +4 + 4− 1, 2 | 4− 1 + 1.
2 | + 1.
Fact (9) is a direct consequence of (7). Moreover, we generalized (9) by induction to obtain (10). Fact (11) is a direct consequence of (8). Perform (9) − (10) + (11) to obtain From here, 1 = 1 so ≡ − implying is not a square.
1 (mod 2). But 2 ≡ 3 (mod 4) so − 1 is a nonresidue
Alternatively, we could have generalized (8) by induction to obtain (12) directly. However, we found that formalizing (12) as we did above was easier since • fact (7) was already generalized to prove Theorem 1; • formalizing a generalization of (8) would have been harder as it was a statement in Lean over integers. So we would have to carefully manipulate the coercion maps from natural numbers to integers.
We formalized the ≡
In this section, we will discuss our formalization of Theorems 1 and 2. Before proving Theorem 1, we proved ∀, ∈ N0, (A) 2 + 2 ̸= 2, (B) > 0 =⇒ ∃, ∈ N0, = 3 · , 3 ∤ , (C) − 1 is a quadratic residue modulo =⇒ ̸≡ 3 (mod 4).
To prove (A), we used quadratic residues modulo 4. Alternatively, we could have proved this using the fact that the diference between consecutive squares is greater than 2 if ̸= 0. However, this would yield a longer formalization due to the inequalities involved. With the latter, the lemma reduces to computing some analogous cases which Lean can easily do with the simp tactic.
We formalized (B) in order to decompose an index for the reduction argument. We proceeded by contradiction. If no such exists then either, 3 | and 3+1 | , or 3 ∤ . However, the latter cannot hold, since 30 | and induction yields 3 | , ∀ ∈ N0. We showed this leads to a contradiction since < 3 but 3 | .
For (C), it was already proved in the number_theory.quadratic_reciprocity library that − 1 is a residue modulo ⇐⇒ ̸≡ 3 (mod 4). (13) Our strategy was to use strong induction. We took two cases depending on whether was prime or not. If was not prime, then from data.nat.prime library, has some prime divisor . Then we know from (13), ̸≡ 3 (mod 4). And for /, we use our induction hypothesis. The problem reduces to checking that the product of two numbers not congruent to 3 (mod 4) is also not congruent to 3 (mod 4).
Perhaps, navigating between diferent representations of remainders was slightly inconvenient. Fact (13) uses data.zmod.basic for integers modulo and field structures over modulo a prime number. On the other hand, some lemmas we used reside in data.nat.modeq. Finally, our lemma (C) needed to be proved as n%4̸=3, a third representation of remainders in Lean.
Proceeding from the step in Theorem 1 after ≡ −
4 (mod ), initially seemed challenging due to division mod , inverses and coercions. We decided to divide both sides by 4 and then showed that /4 ≡ (√/2)2. Using lemmas in zmod.basic allowed us to work with inverses modulo . Then Lean tactics ring and nat.cast lemmas rewrote any expressions with maps between numbers with type zmod and natural numbers.
In this section, we will discuss our formalization of Theorem 3, the main theorem. Before we could begin formalizing Theorem 3, we needed to prove for , , ∈ N, = 2 =⇒ ∃, ∈ N, = gcd(, )2, = gcd(, )2. (14) We did this in two steps; by first proving = 2, gcd(, ) = 1 =⇒ ∃ ∈ N, = 2. (15) Once again, we proved this by strong induction. Take a prime divisor of . Hence | = 2. Then, by a lemma in nat.prime library, | . So 2 | 2 = . We showed by contradiction ∤ (otherwise , are not coprime). Then, we have that gcd(2, ) = 1 directly from a lemma in nat.prime. Lastly, from nat.coprime library we get that 2 | . So, by the induction hypothesis /2 is a square so is a square.
To prove (14), we simply considered and which are coprime from an gcd(, ) gcd(, ) existing lemma in the library. We showed their product is (/ gcd(, ))2 and used (15) twice to complete the proof. Finally, Theorem 3 could be proved easily by inserting the correct lemma at every step of the proof.
Our formalisation of this theorem shows that interactive theorem provers are capable of verifying
non-trivial mathematics. On one hand, powerful tactics make proving routine identities seamless.
On the other hand, higher-order arguments (such as quadratic residues) are handled eficiently
by simply inserting powerful lemmas into relevant parts of a proof. For humans, a complex
theorem is harder to understand and hence verify. For a computer, the verification is no diferent
to that of an easier fact. Perhaps, someday Lean can verify the proof that the only Fibonacci
perfect powers are 0, 1, 8, 144 [
I thank Professor Kevin Buzzard for his guidance and supervision throughout this project.