overview

[kbuzzard]

144 is the largest square in the Fibonacci sequence. This is not going to be completely trivial to prove, because no cheap congruence argument is likely to work: the fact that there are squares in the Fibonacci sequence (namely 0, 1 and 144) means that something more clever will have to be done.

J H E Cohn proved the result in 1963 using relatively elementary methods. A summary of his approach (slightly streamlined) is at

http://wwwf.imperial.ac.uk/~buzzard/2017nt2.pdf

Here are the issues which one will run into when implementing this in Lean.

1) I can prove most of steps 1 and 2 using elementary tricks, however I cannot do all of it, and the most direct proof I know of step 2 (which will also do step 1) is via

https://en.wikipedia.org/wiki/Gauss%27s_lemma_(number_theory)

which uses

https://en.wikipedia.org/wiki/Euler%27s_criterion

which uses the fact that a polynomial (in 1 variable) of degree n over a field has at most n roots, and I don't think this is in Lean. In my mind this will be the longest part to formalise (although I see no difficulties). Mathlib has polynomials in several variables but the 1 variable case is somehow easier and might be a less cluttered approach. The only resource I know for one variable polynomials in Lean is here:

https://github.com/johoelzl/mason-stother/blob/master/poly.lean

but I don't think it goes as far as we need.

2) I think we need to use sqrt(5) along the way, and more precisely (1+-sqrt(5))/2. This means either explicitly building the ring Z[(1+sqrt(5))/2] or using the (noncomputable) reals. The reason for this is that even though steps 4 and 5 can mostly be proved by induction, stuff like step 6 cannot, as far as I know -- one needs step 3. So one has to make a design decision about whether to use the reals with all that entails, or whether to build Z[(1+sqrt(5))/2], which as an abelian group is just Z x Z but with an interesting product.

3) To finish the job we constantly need that every positive integer is uniquely the product of primes, as well as a bunch of elementary facts about congruences which are almost surely in mathlib. I know that Chris Hughes proved the fundamental theorem of Algebra when he was learning Lean here:

https://github.com/kbuzzard/xena/blob/master/student_contributions/Chris_Hughes_FTA.lean

so hopefully the rest is just plumbing.

I am going to try and get all of this done by this coming Saturday lunch time, 26th May 2018! If anyone wants to help they are absoutely welcome.

[kckennylau]

Do we really need sqrt(5)?

[kbuzzard]

One might argue that introducing sqrt(5) is a natural thing to do.

[ChrisHughes24]

FTA is in mathlib now btw.

[kbuzzard]

Here are some details of how the proofs work.

Point 1 and Point 2 both follow from Gauss' lemma after carefully counting, for example, the number of elements of {-2,-4,-6,...,(p-1)} whose "minimal reductions mod p" are negative.

point 3 is a trivial induction which Kenny suggests we might be able to skip.

point 4 is a trivial induction and basic facts about gcd like gcd(a,b)=gcd(a+n*b,b)

point 5 is just computing the fibonacci / lucas sequence mod 3 and 8 [note: we need it mod 16 in point 7], plus observations of the form "a product of primes all of which are 1 or 3 mod 8, is also 1 or 3 mod 8"

beginning of point 6 is where the explicit formula for fib and lucas is most naturally used. One deduces 2u_{m+4n}=um v{4n} + u_{4n} vm, and u{4n} is u{2n} v{2n} is a multiple of v{2n}, whereas v{4n} is -2 mod v_{2n}. The last part is from the result in point 5 that v_2n is odd.

point 7 just follows from a direct computation of fib mod 16. I think it might have period 24 not 12 (from memory) but perhaps u_{12+n} = 9 * u_n and 9 is a square.

In point 8 we're assuming that m can be written in that 4t+q form and showing um isn't a square. The mod v{2n} thing follows from point 6. The prime p is coming from the fact that v_2 is 3 and all higher powers of 2 are 4 or 8 mod 12 so use point 5. The last part comes from point 1. point 9 is now immediate.

[kbuzzard]

In point 10 again we're assuming m is of that form. The congruence mod v{2n} is from point 6 and the fact that u{12} = 144. Note that if p > 3 then -144 is a square mod p iff -1 is a square mod p, as 144 is a square mod p and invertible too. Similarly -288 is a square mod p iff -2 is a square mod p if p>3. The 5,7 mod 8 stuff is coming from point 5.

point 11 follows from point 10 because 12odd = 24x+12 = 8*t+12.

[kbuzzard]

Finally point 12 the first part follows from 11, and coup de grace is that u_{2N} = u_N v_N by point 6 and the gcd of u_N and vN is 1 or 2 by point 4, so this implies that if u{2N} is a square or twice a square, so are u_N and vN. I guess this is subtle to formalise. Here is a suggestion. Prove that the product of two coprime positive integers x and y is a square iff both x and y are -- here you have to use uniqueness of prime factorization and the fact that n is a square iff the power of each prime in the factorization of n is even. Now write u{2N}, v_N etc as a power of 2 times an odd number, apply for the odd numbers, and you're home.

[kbuzzard]

So Kenny if you can do point 6 without sqrt(5) then congratulations, you just obfuscated the proof. From a pedagogical point of view I guess Nicholas' approach is better, but any port in a storm, as they say.

[kckennylau]

Point 4 done.

[kckennylau]

"From a pedagogical point of view I guess Nicholas' approach is better"

I beg to differ. I learnt Fibonacci numbers a long time ago, at a time when I could not even prove the closed forms of Fibonacci. To my mind, Fibonacci numbers belong to a much more elementary level.

[kckennylau]

Just have a look at this website, which even included the identity in Point 6. This is the sort of environment in which I learnt Fibonacci numbers, i.e. when I didn't even know what induction is.