## Stream: maths

### Topic: Largest Square in the Fibonacci Sequence

#### Kevin Buzzard (May 23 2018 at 14:07):

Did you know that 144 is the largest square in the Fibonacci sequence?

#### Kevin Buzzard (May 23 2018 at 14:07):

The proof is elementary but delicate

#### Kevin Buzzard (May 23 2018 at 14:08):

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

#### Kevin Buzzard (May 23 2018 at 14:08):

There is a sketch of the idea

#### Kevin Buzzard (May 23 2018 at 14:08):

I'm giving one such talk on Saturday

#### Kevin Buzzard (May 23 2018 at 14:08):

to the British IMO team

#### Kevin Buzzard (May 23 2018 at 14:08):

and in fact I am giving two talks to these people on Saturday

one on this

#### Kevin Buzzard (May 23 2018 at 14:08):

and one on...whatever I like

#### Kevin Buzzard (May 23 2018 at 14:09):

So I have made the crazy decision to try and give my second talk on a Lean proof of this fact

#### Kevin Buzzard (May 23 2018 at 14:09):

The only problem is that today is Wednesday

#### Kevin Buzzard (May 23 2018 at 14:09):

which means that it's only three days to Saturday

So I did this

#### Kevin Buzzard (May 23 2018 at 14:09):

https://github.com/kbuzzard/lean-squares-in-fibonacci/issues/1

#### Kevin Buzzard (May 23 2018 at 14:09):

and I will start this evening

#### Kevin Buzzard (May 23 2018 at 14:10):

but if anyone wants to help

#### Kevin Buzzard (May 23 2018 at 14:10):

then I would happily let them join in

#### Kevin Buzzard (May 23 2018 at 14:10):

give them push access, whatever

#### Kevin Buzzard (May 23 2018 at 14:10):

The link to the issues makes it clear what I think the problems are

#### Kevin Buzzard (May 23 2018 at 14:10):

(1) We either cheat and assume some UG-level facts about primes

#### Kevin Buzzard (May 23 2018 at 14:10):

(when -2 is a square mod p)

or we prove it

#### Kevin Buzzard (May 23 2018 at 14:11):

which will involve proving that a poly of degree n over a field has at most n roots

#### Kevin Buzzard (May 23 2018 at 14:11):

and that Z/pZ is a field

#### Kevin Buzzard (May 23 2018 at 14:11):

(2) we either use the real numbers or build our own Z[(1+sqrt(5))/2]

#### Kevin Buzzard (May 23 2018 at 14:11):

(3) a bunch of relatively simple arithmetic

#### Kevin Buzzard (May 23 2018 at 14:11):

but a fair amount of it, from a Lean point of view

#### Kevin Buzzard (May 23 2018 at 14:12):

I attained my schemes goal

#### Kevin Buzzard (May 23 2018 at 14:12):

so I want to spend a few days goofing around with this one

#### Kevin Buzzard (May 23 2018 at 14:12):

it's very easy arithmetic

#### Kevin Buzzard (May 23 2018 at 14:12):

and maybe I will do it all myself

#### Kevin Buzzard (May 23 2018 at 14:12):

but if anyone wants to help

#### Kevin Buzzard (May 23 2018 at 14:12):

this would be greatly appreciated :-)

#### Kevin Buzzard (May 23 2018 at 14:13):

@Johannes Hölzl and @Chris Hughes I might have to steal your work (with attribution of course).

#### Kevin Buzzard (May 23 2018 at 14:15):

Johannes -- who do I credit if I take your polynomial stuff from mason-stothers? [or mason-stother as you seem to have called it]? Is it you or JWageM?

#### Kevin Buzzard (May 23 2018 at 14:15):

I firmly believe I could do this entire thing in 3 days

#### Kevin Buzzard (May 23 2018 at 14:15):

it's a bit unfortunate about the marking I still have to do though :-/

#### Kevin Buzzard (May 23 2018 at 14:16):

Chris and Kenny will have finished their exams by Friday afternoon UK time so this would be a perfect all-night binge for them to do afterwards.

;-)

#### Kevin Buzzard (May 23 2018 at 14:16):

OK now back to marking

#### Johannes Hölzl (May 23 2018 at 14:19):

Mason-stother's polynomials are from us both, most parts were done by Jens, some by me. Its okay to only credit Jens.

#### Nicholas Scheel (May 23 2018 at 15:01):

Hi! How can I help best? Maybe start building Z[(1+sqrt(5))/2] ? I have a little experience with field extensions from abstract algebra this past semester ...

#### Nicholas Scheel (May 23 2018 at 15:03):

that’s really just Z[sqrt(5)] right? field operations will get you (1+-sqrt(5))/2 from that

#### Patrick Massot (May 23 2018 at 15:03):

He wants a ring, not a field

#### Patrick Massot (May 23 2018 at 15:03):

And that's what this notation denotes

#### Kevin Buzzard (May 23 2018 at 15:10):

Right -- there is Q(sqrt(5)) = Q(alpha) [alpha := (1+sqrt(5))/2] and there is Z[sqrt(5)] which is strictly smaller than Z[alpha] [it has index 2]

#### Kevin Buzzard (May 23 2018 at 15:11):

The only reason I suggested the ring not the field was (1) rings have fewer axioms than fields and (2) my instinct was to construct the smallest object which was mathematically reasonable [so no semirings or distribs, thank you] and which contained enough to formalise the statement "u_m = (alpha^m - beta^m) / sqrt (5)"...oh crap

#### Kevin Buzzard (May 23 2018 at 15:11):

maybe a field is fine :-)

#### Kevin Buzzard (May 23 2018 at 15:11):

One could prove sqrt(5) * u_m = alpha^m - beta^m

#### Kevin Buzzard (May 23 2018 at 15:12):

and then mumble about integral domains

#### Kevin Buzzard (May 23 2018 at 15:12):

OK so @Nicholas Scheel if you want to take a look at how the complex numbers were built from the real numbers in mathlib (in some file called complex.lean probably) then you could just copy this and build Q(sqrt(5)) from Q by adjoining a square root of 5

#### Kevin Buzzard (May 23 2018 at 15:13):

The only difficulty will be in proving that if a+b*sqrt(5) is non-zero then a^2-5b^2 is non-zero, which you need for division

#### Kevin Buzzard (May 23 2018 at 15:13):

For the complexes the argument is that everything is positive, that doesn't work here

#### Kevin Buzzard (May 23 2018 at 15:13):

you need that 5 isn't the square of a rational

#### Kevin Buzzard (May 23 2018 at 15:13):

but modulo that, there's your Q(sqrt(5))

#### Kevin Buzzard (May 23 2018 at 15:13):

at some point one would need this anyway, to prove Z[alpha] is an integral domain, so there's no getting away from it

#### Chris Hughes (May 23 2018 at 15:33):

I've done some stuff on integers mod n which I'll send you when I get home.

#### Nicholas Scheel (May 23 2018 at 15:48):

Ah okay, I see ... I think I'll try to build Z[alpha], doesn't look like we'll need division

#### Chris Hughes (May 23 2018 at 16:52):

@Kevin Buzzard Very messy, but the most basic stuff about integers mod n is there. https://github.com/dorhinj/leanstuff/blob/master/Zmod1.lean

#### Chris Hughes (May 23 2018 at 16:53):

@Nicholas Scheel I also made a bit of a start on univariate polys, although I haven't done much more than copy Johannes stuff on multivariate polys.

#### Chris Hughes (May 23 2018 at 16:54):

I think Sean's finset.max would be a more appropriate definition of degree than sup

#### Nicholas Scheel (May 23 2018 at 16:57):

okay I have a commutative ring instance for Z[alpha]!

#### Johannes Hölzl (May 23 2018 at 16:59):

with sup you don't need to use iget. max is the better name but I think sup has the better behaviour.

#### Patrick Massot (May 23 2018 at 18:25):

Thanks, but I don't know how to use sup

#### Kenny Lau (May 23 2018 at 18:52):

@Kevin Buzzard have you pushed?

pushed what?

fibonacci

#### Kevin Buzzard (May 23 2018 at 18:56):

Chris -- Johannes and his student wrote some univariate poly stuff in their mason-stother repo

#### Kevin Buzzard (May 23 2018 at 18:57):

What Fibonacci is there for me to push?

I have epsilon

#### Kevin Buzzard (May 23 2018 at 18:57):

I proved luc (m + 3) = 2 * fib (m + 3) + fib m

#### Kevin Buzzard (May 23 2018 at 18:57):

I will push some stuff

#### Chris Hughes (May 23 2018 at 19:00):

They didn't do the theorem you need I don't think.

#### Kevin Buzzard (May 23 2018 at 19:11):

I pushed some stuff

#### Kevin Buzzard (May 23 2018 at 19:12):

I proved 2/3 of point 4

#### Kevin Buzzard (May 23 2018 at 19:55):

Is gcd (a + n * b) b = gcd a b in lean or mathlib somewhere? (everything a nat)]

#### Patrick Massot (May 23 2018 at 19:55):

If everything is a nat, this is almost certainly wrong in some edge case

#### Kenny Lau (May 23 2018 at 19:58):

there isn't, since gcd is well-defined for 0 in the real world

#### Patrick Massot (May 23 2018 at 20:00):

I knew it: edge case

#### Kenny Lau (May 23 2018 at 20:00):

#check nat.gcd_rec -- nat.gcd m n = nat.gcd (n % m) m
open nat
example (a n b : ℕ) : gcd (a + n * b) b = gcd a b :=
by rw [gcd_comm, gcd_rec, add_mul_mod_self_right, ← gcd_rec, gcd_comm]


#### Kenny Lau (May 23 2018 at 20:00):

there is no edge case!

#### Patrick Massot (May 23 2018 at 20:01):

This is an edge case to the general statement that every general statement about nat is wrong

#### Kevin Buzzard (May 23 2018 at 20:09):

of course one could argue that gcd 0 0 = 0 is already wrong

#### Kevin Buzzard (May 23 2018 at 20:09):

given that 7 divides both 0 and 0

#### Patrick Massot (May 23 2018 at 20:11):

To be honest, that one has nothing to do with nat. It's also a problem in integers

#### Kevin Buzzard (May 23 2018 at 20:12):

You know that $\frac{\zeta(1-k)}{2} + \Sigma_{n\geq1}\sigma_{k-1}(n)q^n$ is a modular form, right?

#### Kevin Buzzard (May 23 2018 at 20:13):

Here $\sigma_{k-1}(n)$ denotes the sum of the $k-1$ st powers of the positive divisors of $n$.

#### Kevin Buzzard (May 23 2018 at 20:14):

but if you set $n=0$ in the sum you get the sum of the $k-1$ st powers of the positive divisors of $0$

#### Kevin Buzzard (May 23 2018 at 20:14):

so that's $1^{k-1} + 2 ^{k-1} + 3^{k-1} + \cdots$

#### Kevin Buzzard (May 23 2018 at 20:14):

which is $\zeta(1-k)$ by...erm...definition...or something

#### Kevin Buzzard (May 23 2018 at 20:15):

but the sum is only over half of the integers

#### Kevin Buzzard (May 23 2018 at 20:15):

so you should only take the term at zero half as seriously

#### Kevin Buzzard (May 23 2018 at 20:15):

which gives you $\zeta(1-k)/2$

#### Kevin Buzzard (May 23 2018 at 20:15):

and that's how I remember it

#### Patrick Massot (May 23 2018 at 20:16):

And we are surprised formalizing maths is hard...

#### Nicholas Scheel (May 23 2018 at 20:19):

@Kevin Buzzard Should I make a fork, or may I have commit access?

#### Kenny Lau (May 23 2018 at 20:19):

do I have commit access?

#### Kevin Buzzard (May 23 2018 at 20:21):

what is the most sensible idea?

#### Kevin Buzzard (May 23 2018 at 20:21):

nobody has commit access except me

#### Kevin Buzzard (May 23 2018 at 20:21):

but I am happy to give it to anybody

#### Kevin Buzzard (May 23 2018 at 20:21):

unless someone has a good reason why I shouldn't do this

#### Kenny Lau (May 23 2018 at 20:22):

I'll kindly delete your alpha and beta :P (after proving points 4 and 6)

#### Patrick Massot (May 23 2018 at 20:22):

If I were you I would fear seeing constructive stuff invading my repo

#### Kevin Buzzard (May 23 2018 at 20:24):

OK Kenny and Nicholas you should have push access

thanks

#### Kenny Lau (May 23 2018 at 20:24):

If I were you I would fear seeing constructive stuff invading my repo

much fear of the unknown :P

#### Kevin Buzzard (May 23 2018 at 20:24):

but lemme push some stuff

#### Kevin Buzzard (May 23 2018 at 20:24):

I need a job done

OK I am pushed

#### Kenny Lau (May 23 2018 at 20:27):

waitttt where did the Z alpha come from

#### Kenny Lau (May 23 2018 at 20:27):

oh Nicholas built it...

#### Kenny Lau (May 23 2018 at 20:27):

@Nicholas Scheel do you think we'll really need it?

#### Nicholas Scheel (May 23 2018 at 20:27):

oops sorry, did I step on your push?

no

#### Kenny Lau (May 23 2018 at 20:28):

I'm just doubting whether we need sqrt(5) at all

#### Kevin Buzzard (May 23 2018 at 20:28):

Here's the reason I think we might need sqrt(5)

#### Nicholas Scheel (May 23 2018 at 20:28):

I think this might help along the way ;) :

lemma αβsum : α + β = 1 := rfl
lemma αβprod : α * β = -1 := rfl


#### Kevin Buzzard (May 23 2018 at 20:28):

that looks really good

#### Kevin Buzzard (May 23 2018 at 20:29):

it's a little bit better than my method

#### Kenny Lau (May 23 2018 at 20:29):

so, constructivism wins?

#### Kevin Buzzard (May 23 2018 at 20:29):

To prove something like luc (m + 3) = 2 * fib (m + 3) + fib m you can just do it by induction

#### Kevin Buzzard (May 23 2018 at 20:29):

but to prove luc (4 * n) = (luc (2 * n) ^ 2) - 2

#### Kevin Buzzard (May 23 2018 at 20:30):

the only method I know is to prove the general sqrt (5) formula

#### Kenny Lau (May 23 2018 at 20:30):

you just need the right lemmas

#### Kevin Buzzard (May 23 2018 at 20:30):

maybe some theorem of logic says you don't need square roots of 5

#### Kenny Lau (May 23 2018 at 20:30):

like the one I proved that day

#### Kenny Lau (May 23 2018 at 20:30):

variables (m n : ℕ)

local attribute [elab_as_eliminator] nat.strong_induction_on

theorem to_be_named : fib (m + n + 1) =
fib m * fib n + fib (m + 1) * fib (n + 1) :=
nat.strong_induction_on n $λ n, nat.cases_on n (λ _, by simp [fib])$ λ n,
nat.cases_on n (λ _, by simp [fib]) $λ n ih, have H1 : _ := ih n (nat.lt_trans (nat.lt_succ_self n) (nat.lt_succ_self (n+1))), have H2 : fib (m + n + 2) = _ + _ * (fib n + fib (n+1)) := ih (n+1) (nat.lt_succ_self (n+1)), calc fib (m + n + 1) + fib (m + n + 2) = fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) : by rw [H1, H2, mul_add, mul_add, mul_add, mul_add]; ac_refl  #### Kevin Buzzard (May 23 2018 at 20:30): but then you will end up defining some auxiliary function on Z x Z #### Kevin Buzzard (May 23 2018 at 20:30): Let me just read through the proof #### Kevin Buzzard (May 23 2018 at 20:31): Of course one might also argue that using sqrt(5) is a _natural_ thing to do #### Kevin Buzzard (May 23 2018 at 20:31): which might make it a good thing to do #### Kenny Lau (May 23 2018 at 20:32): I should add "building the algebraic numbers" to my want-to-do-but-god-knows-when list #### Kevin Buzzard (May 23 2018 at 20:32): Of course you could also take the ring Q[x] and quotient out by the ideal (x^2-5) right? ;-) #### Kevin Buzzard (May 23 2018 at 20:33): I will write comments about the proof in the issue #### Patrick Massot (May 23 2018 at 20:35): From an arithmetic point of view it makes much more sense than defining square root on nonnegative reals #### Mario Carneiro (May 23 2018 at 20:39): Hey, it might be too late for this remark but I built the ring Z[\sqrt n] in pell.lean. Not directly applicable, but it might be useful #### Mario Carneiro (May 23 2018 at 20:43): of course one could argue that gcd 0 0 = 0 is already wrong given that 7 divides both 0 and 0 I think there are good reasons to believe that gcd 0 0 = 0 is right over both nat and int, and in traditional math, if you think about the integers in that calculation as representing their principal ideals. (gcd m n) = (m, n) #### Mario Carneiro (May 23 2018 at 20:44): so here "greatest" actually means greatest in the divisor order, putting 0 at the top not the bottom #### Kenny Lau (May 23 2018 at 20:48): @Kevin Buzzard 7 divides both 0 and 0, and 7 divides gcd(0,0) = 0, consistent with the UMP of GCD #### Kenny Lau (May 23 2018 at 20:56): @Kevin Buzzard can I push? #### Kevin Buzzard (May 23 2018 at 20:57): sure go ahead and push #### Kevin Buzzard (May 23 2018 at 20:57): I wrote a more detailed sketch of how to flesh out the argument in the issue #### Kenny Lau (May 23 2018 at 20:58): are you sure I have write access? #### Kevin Buzzard (May 23 2018 at 20:58): I need to go and steer my children towards their beds now. Thanks for the help all of you. Mario and Kenny, I see the advantages of the "zero bigger than everything" approach here! Of course it's just the ideal-theoretic way of thinking about it -- gcd(x,y) = ideal generated by x and y, and if it's principal then let's choose a canonical generator if we can. #### Kevin Buzzard (May 23 2018 at 20:58): Kenny I think I invited you. Did you check your email or did I fail? #### Kenny Lau (May 23 2018 at 20:59): oh, I need to accept the invitation #### Kevin Buzzard (May 23 2018 at 20:59): https://github.com/kbuzzard/lean-squares-in-fibonacci/issues/1 #### Kevin Buzzard (May 23 2018 at 20:59): Note the last part -- point 12 is slightly delicate, it needs the following consequence of uniqueness of prime factorization: if gcd(x,y)=1 and x*y is a square then x and y are both squares (here x,y>0). #### Kevin Buzzard (May 23 2018 at 21:01): and for that you need: n square iff v_p(n) even for all primes p (v_p(n) = largest power of p dividing n) and gcd(x,y)=1 iff min(v_p(x),v_p(y))=0 for all primes p #### Mario Carneiro (May 23 2018 at 21:03): pretty sure that exact theorem is in my formalization #### Mario Carneiro (May 23 2018 at 21:04): and you don't need UFD for it #### Kevin Buzzard (May 23 2018 at 21:05): well you do need something #### Kevin Buzzard (May 23 2018 at 21:05): because it's not true in a general ring #### Kevin Buzzard (May 23 2018 at 21:05): well I suppose it depends on what you mean by gcd in a general ring #### Mario Carneiro (May 23 2018 at 21:05): you need nat.gcd facts and some induction #### Mario Carneiro (May 23 2018 at 21:06): I'm not saying it doesn't depend in a reverse mathematics way on UFD, but you don't need all that complexity for the proof #### Kevin Buzzard (May 23 2018 at 21:06): a bit like the proof of UFD ;-) #### Kevin Buzzard (May 23 2018 at 21:06): [I mean, you need nat.gcd facts and some induction for that too] #### Kevin Buzzard (May 23 2018 at 21:07): For a general comm ring there are two natural defs of gcd, one more general than the other #### Kevin Buzzard (May 23 2018 at 21:07): and the weaker version of coprime doesn't cut it #### Kevin Buzzard (May 23 2018 at 21:07): oh there are also issues with units #### Kevin Buzzard (May 23 2018 at 21:07): -4 and -9 are coprime and their product is a square etc etc #### Kevin Buzzard (May 23 2018 at 21:08): so there are issues in general #### Kevin Buzzard (May 23 2018 at 21:08): but I take your point that you are saying you don't have to go through v_p(x) #### Mario Carneiro (May 23 2018 at 21:08): right #### Mario Carneiro (May 23 2018 at 21:08): it's a nice way to conceptualize it, but it's technically complicated and not worth it for most problems IMO #### Mario Carneiro (May 23 2018 at 21:10): whenever you need a fact that would come from primality of the p in v_p(n), just use the coprime assumption instead, it's just as well for the purpose of the proof #### Kenny Lau (May 23 2018 at 21:23): @Mario Carneiro what's the fastest way to know that n=1 or n=2 given n divides 2? #### Mario Carneiro (May 23 2018 at 21:23): n | 2 implies n <= 2 #### Chris Hughes (May 23 2018 at 21:23): 2 is prime #### Mario Carneiro (May 23 2018 at 21:23): alternatively, 2 is prime #### Kenny Lau (May 23 2018 at 21:23): oh lol #### Kenny Lau (May 23 2018 at 21:32): Point 4 done! #### Nicholas Scheel (May 23 2018 at 22:42): I want to prove this but I don't know how? lemma Fib.is_fib (n : ℤ) : Fib (n+2) = Fib n + Fib (n + 1) :P #### Nicholas Scheel (May 23 2018 at 22:42):  cases n, refl, induction n using nat.case_strong_induction_on with n ih, refl, cases n, refl, cases n, refl, have ih0 := ih n (nat.le_succ_of_le (nat.le_succ _)), have ih1 : Fib (-[1+n+1] + 2) = Fib -[1+n+1] + Fib -[1+n] := ih (n+1) (nat.le_succ _), have ih2 : Fib -[1+n] = Fib -[1+n+2] + Fib -[1+n+1] := ih (n+2) (le_refl _),  #### Kenny Lau (May 23 2018 at 22:43): write x^(n+2) as x^n x^2? #### Kenny Lau (May 23 2018 at 22:43): you might find int.induction_on useful #### Kenny Lau (May 24 2018 at 02:44): Point 6 done except the last claim #### Kevin Buzzard (May 24 2018 at 07:39): OK this is great. #### Kevin Buzzard (May 24 2018 at 07:39): Looking at what has been already done #### Kevin Buzzard (May 24 2018 at 07:39): I already easily have enough material to fill the session. #### Kevin Buzzard (May 24 2018 at 07:39): So actually the time pressure is over. #### Kevin Buzzard (May 24 2018 at 07:40): These kids are smart kids (my audience of 8) #### Kevin Buzzard (May 24 2018 at 07:40): but the Lean session will last 90 minutes #### Kevin Buzzard (May 24 2018 at 07:40): and even talking about how to construct Z[alpha] and computing Fibonacci numbers mod n throws up so much stuff #### Kevin Buzzard (May 24 2018 at 07:41): that my talk is already written. #### Kevin Buzzard (May 24 2018 at 07:41): However I am definitely still interested in finishing the job :-) #### Kevin Buzzard (May 24 2018 at 07:41): Here's a question. #### Kevin Buzzard (May 24 2018 at 07:42): Oh -- before I start -- thanks to Kenny and Nicholas for their contributions! #### Kevin Buzzard (May 24 2018 at 07:42): I'm still mired in marking and preparing these talks for Sat was beginning to become a worry. #### Kevin Buzzard (May 24 2018 at 07:43): The question is how to express the following assertion in Lean #### Kevin Buzzard (May 24 2018 at 07:43): We need to compute the Fibonacci sequence mod 16 #### Kevin Buzzard (May 24 2018 at 07:44): The theorem is that mod 16 it goes like this: #### Kevin Buzzard (May 24 2018 at 07:44): [0, 1, 1, 2, 3, 5, 8, 13, 5, 2, 7, 9, 0, 9, 9, 2, 11, 13, 8, 5, 13, 2, 15, 1] #### Kevin Buzzard (May 24 2018 at 07:45): And the proof is "trivial by induction" #### Kevin Buzzard (May 24 2018 at 07:45): (because each term in that list is the sum of the previous two terms mod 16, and at the end we have 15 + 1 = 0 and 1 + 0 = 1 so we wrap back) #### Kevin Buzzard (May 24 2018 at 07:46): The question is how one can prove this in Lean in a way which actually looks reasonable #### Kevin Buzzard (May 24 2018 at 07:46): This is not a question about how to do anything mod n, this is a specific question about mod 16 (there's an analogous one for mod 3 but I chose the most awkward one). #### Kevin Buzzard (May 24 2018 at 07:46): One issue is what to do the induction on. #### Kevin Buzzard (May 24 2018 at 07:47): You could do strong induction on m #### Kevin Buzzard (May 24 2018 at 07:47): or you could write m = 24 * n + t with 0 <= t < 24 and do induction on n #### Kevin Buzzard (May 24 2018 at 07:48): What I am (not really that) concerned about is that with either approach you end up writing essentially the same code block 24 or so times #### Kevin Buzzard (May 24 2018 at 07:50): In the direct strong induction argument you case on n mod 24 and I don't really know how to do that #### Kevin Buzzard (May 24 2018 at 07:50): hmm #### Kevin Buzzard (May 24 2018 at 07:50): maybe it's OK #### Kevin Buzzard (May 24 2018 at 07:51): if t < 22 it's some lemma of the form (a+b)%m = (a%m+b%m)%m -- is that in Lean/mathlib? #### Kevin Buzzard (May 24 2018 at 07:51): and in the induction case you end up with a statement of the form a0 and a1 and ... and a23 #### Kevin Buzzard (May 24 2018 at 07:51): you would never write such a statement in python or whatever, you would somehow wrap everything up in a list #### Kevin Buzzard (May 24 2018 at 07:52): Hmm #### Kevin Buzzard (May 24 2018 at 07:52): I think my question is that I am seeing two competing methods for proving this and they book look a bit "trivial in maths but a bit ugly to write in Lean" at the minute. Anyone have any suggestions? #### Chris Hughes (May 24 2018 at 07:55): if t < 14 it's some lemma of the form (a+b)%m = (a%m+b%m)%m -- is that in Lean/mathlib? int.modeq.modeq_add should help, since this is defeq to a + b \== a%m + b % m Although I forgot modeq_mod i.e. , so you'll have to prove that. Why not just prove it as a lemma about integers mod n, and not naturals. #### Kevin Buzzard (May 24 2018 at 07:57): The problem with working with integers mod n is that if you want the _input_ to fib to be an integer mod n (n would be 24 here) then you have to prove that your definition is well-defined. #### Kevin Buzzard (May 24 2018 at 07:57): and that's basically the same question, or another way of writing it, as far as I can see. Am I missing your point? #### Kevin Buzzard (May 24 2018 at 07:57): Oh -- or are you just talking about the (a+b)%m lemma? #### Chris Hughes (May 24 2018 at 07:58): The definition is just quot.mk \circ fib #### Kevin Buzzard (May 24 2018 at 07:58): Chris I'm talking about the input not the output #### Chris Hughes (May 24 2018 at 07:58): I'm talking about the mod 16 lemma #### Kevin Buzzard (May 24 2018 at 07:58): I can get fib : N -> N / 16 fine #### Kevin Buzzard (May 24 2018 at 07:58): But fib : (N / 24) -> N / 16 is less fine #### Kevin Buzzard (May 24 2018 at 07:58): what am I saying #### Kevin Buzzard (May 24 2018 at 07:58): what has happened to me #### Kevin Buzzard (May 24 2018 at 07:58): (Z / 24) #### Chris Hughes (May 24 2018 at 07:59): Just do nat \r mod 16 #### Kevin Buzzard (May 24 2018 at 07:59): what the hell is N mod 24 #### Kevin Buzzard (May 24 2018 at 07:59): I understand how to build fib : N -> Z / 16 #### Kevin Buzzard (May 24 2018 at 07:59): The issue is proving that fib (n + 24) = fib n #### Kevin Buzzard (May 24 2018 at 08:00): The only proof I know of that statement is #### Kevin Buzzard (May 24 2018 at 08:00): "consider n mod 24" #### Kevin Buzzard (May 24 2018 at 08:00): Oh #### Kevin Buzzard (May 24 2018 at 08:00): I realised I made a mistake above #### Kevin Buzzard (May 24 2018 at 08:00): I am going to edit a bunch of 16s and change them to 24s #### Kevin Buzzard (May 24 2018 at 08:00): input mod 24, output mod 16 #### Kevin Buzzard (May 24 2018 at 08:02): OK fixed #### Kevin Buzzard (May 24 2018 at 08:02): So the issue is proving a = b mod 24 implies fib a = fib b mod 16 #### Kevin Buzzard (May 24 2018 at 08:02): hmm #### Kevin Buzzard (May 24 2018 at 08:03): this is an idea #### Kevin Buzzard (May 24 2018 at 08:03): one can prove fib (n + 24) = fib n mod 16 #### Kevin Buzzard (May 24 2018 at 08:03): by induction on n #### Kevin Buzzard (May 24 2018 at 08:03): and one has to hope that Lean has the firepower to compute fib 24 #### Kevin Buzzard (May 24 2018 at 08:03): to get the induction started #### Kevin Buzzard (May 24 2018 at 08:03): OK so #### Kevin Buzzard (May 24 2018 at 08:03): actually #### Kevin Buzzard (May 24 2018 at 08:04): one can define fibmod16 #### Kevin Buzzard (May 24 2018 at 08:04): I see #### Kevin Buzzard (May 24 2018 at 08:04): fibmod16 : N -> Z/16 #### Kevin Buzzard (May 24 2018 at 08:04): then prove that forall n, fibmod16 (n + 24) = fibmod16 n by induction on n #### Kevin Buzzard (May 24 2018 at 08:04): and now no firepower needed #### Kevin Buzzard (May 24 2018 at 08:05): and now prove fib mod 16 is fibmod16 by induction on n #### Kevin Buzzard (May 24 2018 at 08:05): and you're done! #### Kevin Buzzard (May 24 2018 at 08:05): This is great! #### Kevin Buzzard (May 24 2018 at 08:05): Thanks Chris! #### Kevin Buzzard (May 24 2018 at 08:05): I could even make that discussion into 90 minutes, given that none of the kids will have seen Lean before #### Chris Hughes (May 24 2018 at 08:06): induction, bases case rfl, next case unfold 24 times, and hope things simplify #### Kevin Buzzard (May 24 2018 at 08:08): Yeah I think you've cracked it. Thanks Chris. #### Kevin Buzzard (May 24 2018 at 08:08): Now get back to stats revision ;-) #### Kenny Lau (May 24 2018 at 09:05): The correct way is to use the theorem I proved that day :P #### Kevin Buzzard (May 24 2018 at 09:06): Kenny #### Kevin Buzzard (May 24 2018 at 09:06): your comments are sometimes obscure #### Kevin Buzzard (May 24 2018 at 09:06): but "the theorem I proved that day" will take some beating #### Kevin Buzzard (May 24 2018 at 09:06): (a%m+b%m)%m=(a+b)%m is horrible #### Kenny Lau (May 24 2018 at 09:06): theorem to_be_named : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) := nat.strong_induction_on n$ λ n, nat.cases_on n (λ _, by simp [fib]) $λ n, nat.cases_on n (λ _, by simp [fib])$ λ n ih,
have H1 : _ := ih n (nat.lt_trans (nat.lt_succ_self n) (nat.lt_succ_self (n+1))),
have H2 : fib (m + n + 2) = _ + _ * (fib n + fib (n+1)) := ih (n+1) (nat.lt_succ_self (n+1)),
calc  fib (m + n + 1) + fib (m + n + 2)
= fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) :


#### Kenny Lau (May 24 2018 at 09:06):

it's how it's done in proofwiki

#### Kenny Lau (May 24 2018 at 09:07):

this lemma, plus the fact that fib 16 and fib 17 are coprime

#### Kevin Buzzard (May 24 2018 at 09:07):

OK so I will now home in on the other part of your sentence

#### Kevin Buzzard (May 24 2018 at 09:07):

"The correct way"

#### Kenny Lau (May 24 2018 at 09:07):

it's more general

#### Kenny Lau (May 24 2018 at 09:07):

you can prove that fib m | fib n iff m | n

#### Kevin Buzzard (May 24 2018 at 09:07):

Oh so you're just talking about the correct way to do something random

#### Kevin Buzzard (May 24 2018 at 09:08):

I was rather hoping you were talking about the thing I was interested in :-)

m = 16?

Oh yeah!

#### Kenny Lau (May 24 2018 at 09:08):

that's a special case lol

#### Chris Hughes (May 24 2018 at 09:08):

this lemma, plus the fact that fib 16 and fib 17 are coprime

Is this easy to prove, or are the numbers too big for lean to handle?

#### Kevin Buzzard (May 24 2018 at 09:08):

fib n is coprime to fib (n+1)

#### Kenny Lau (May 24 2018 at 09:08):

this lemma, plus the fact that fib 16 and fib 17 are coprime

Is this easy to prove, or are the numbers too big for lean to handle?

#### Kevin Buzzard (May 24 2018 at 09:08):

by Euclid's algorithm

#### Kevin Buzzard (May 24 2018 at 09:09):

I can't face (a%m+a%m)%m=(a+b)%m

#### Kevin Buzzard (May 24 2018 at 09:09):

I am going to work with Z/n

#### Kevin Buzzard (May 24 2018 at 09:09):

Where is this in Lean?

I currently have

#### Kevin Buzzard (May 24 2018 at 09:10):

definition fib_mod (m : ℕ) : ℕ → ℕ
| 0 := 0 % m
| 1 := 1 % m
| (n + 2) := ( (fib_mod n) + (fib_mod (n + 1)) ) % m


#### Kevin Buzzard (May 24 2018 at 09:10):

but I am going to go for a map from N to whatever Z/nZ is called

#### Kevin Buzzard (May 24 2018 at 09:10):

as long as it's an abelian group

#### Kevin Buzzard (May 24 2018 at 09:11):

oh so it's not in Lean?

No.

I mean mathlib

OK

I will steal it

#### Kevin Buzzard (May 24 2018 at 09:11):

you only did Z mod 1?

#### Chris Hughes (May 24 2018 at 09:12):

The 1 is to distinguish it from another construction I did.

Oh OK :-)

That's a relief

#### Kevin Buzzard (May 24 2018 at 09:12):

I was hoping for Zmod16

wow

#### Kevin Buzzard (May 24 2018 at 09:13):

https://github.com/dorhinj/leanstuff

#### Kevin Buzzard (May 24 2018 at 09:13):

you have been pretty productive in the last 16 hours

lol

it's Chrislib

#### Kevin Buzzard (May 24 2018 at 09:14):

I like the look of kbuzzard.lean

#### Kevin Buzzard (May 24 2018 at 09:14):

Is that one of my theorems?

#### Kevin Buzzard (May 24 2018 at 09:15):

Actually, hopefully, one of my theorems really _will_ be in Lean soon

#### Kevin Buzzard (May 24 2018 at 09:15):

Ellen is going to formalize my dots and boxes paper

#### Kevin Buzzard (May 24 2018 at 09:22):

If Z mod n isn't in mathlib and requires a bunch of Chris' local imports it might be easier to just go for def nat.mod_add (a b m : ℕ) : (a % m + b % m) % m = (a + b) % m := sorry

#### Kevin Buzzard (May 24 2018 at 09:22):

I am not enough of an expert in how to use % to see how to prove this

#### Kevin Buzzard (May 24 2018 at 09:22):

and it doesn't appear to be there already

#### Kevin Buzzard (May 24 2018 at 09:23):

KB <- professional number theorist who is not an expert in mod

:-/

#### Kevin Buzzard (May 24 2018 at 09:24):

I added the sorried assertion to https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/definitions.lean

#### Chris Hughes (May 24 2018 at 09:27):

@[simp] lemma nat.mod_mod (n m : ℕ) : n % m % m = n % m :=
nat.cases_on m (by simp) (λ m, mod_eq_of_lt (mod_lt _ (succ_pos _)))

def nat.mod_add (a b m : ℕ) : (a % m + b % m) % m = (a + b) % m :=
nat.modeq.modeq_add (nat.mod_mod _ _) (nat.mod_mod _ _)


#### Patrick Massot (May 24 2018 at 09:28):

This is becoming slightly creepy

#### Patrick Massot (May 24 2018 at 09:28):

Kevin, what have you created?

#### Kenny Lau (May 24 2018 at 09:31):

import definitions

theorem fib_add (m n : ℕ) : fib (m + n + 1) =
fib m * fib n + fib (m + 1) * fib (n + 1) :=
nat.rec_on_two n (by unfold fib; rw [mul_zero, zero_add, mul_one]; refl)
(by unfold fib; rw [zero_add, mul_one, mul_one]; refl) $λ n ih1 ih2, calc fib (m + n + 1) + fib (m + nat.succ n + 1) = fib m * (fib n + fib (n+1)) + fib (m+1) * (fib (n+1) + (fib n + fib (n+1))) : by rw [ih1, ih2, fib, mul_add, mul_add, mul_add, mul_add, nat.succ_eq_add_one]; ac_refl attribute [refl] dvd_refl attribute [trans] dvd_trans theorem fib_dvd_mul (m n : ℕ) : fib m ∣ fib (m * n) := nat.cases_on m (by rw [zero_mul]; refl)$ λ m,
nat.rec_on n (dvd_zero _) $λ n ih, show fib (nat.succ m) ∣ fib (nat.succ m * n + m + 1), by rw [fib_add]; apply dvd_add; [apply dvd_mul_of_dvd_left ih, apply dvd_mul_left]  #### Kenny Lau (May 24 2018 at 09:31): done #### Kenny Lau (May 24 2018 at 09:31): I don't need the fact that fib m and fib m+1 are coprime #### Kenny Lau (May 24 2018 at 09:32): I would need it to prove the converse though #### Kevin Buzzard (May 24 2018 at 09:33): Kevin, what have you created? This is the new normal. Professors who can't prove things about mod so they ask the undergraduates #### Kevin Buzzard (May 24 2018 at 09:34): I really want that by December there are a bunch of undergraduates at my university asking their tutors questions which the tutors can't answer #### Kevin Buzzard (May 24 2018 at 09:34): or showing them code which the tutors can't understand #### Kevin Buzzard (May 24 2018 at 09:34): or saying "I typed up your problem sheet into Lean and you made an off by one error" #### Kenny Lau (May 24 2018 at 09:34): pushed #### Kevin Buzzard (May 24 2018 at 09:34): Thanks Kenny #### Kevin Buzzard (May 24 2018 at 09:35): I need a recursor for % #### Kevin Buzzard (May 24 2018 at 09:35): If I have a function F from nat to X #### Kevin Buzzard (May 24 2018 at 09:35): and a proof that F (n + 24) = F n #### Kevin Buzzard (May 24 2018 at 09:35): then I want a theorem that F n = F (n % 24) #### Kevin Buzzard (May 24 2018 at 09:35): Is that a recursor? #### Kevin Buzzard (May 24 2018 at 09:35): It's what I want, at any rate #### Kenny Lau (May 24 2018 at 09:36): ok a minute #### Kevin Buzzard (May 24 2018 at 09:36): what I don't want #### Kevin Buzzard (May 24 2018 at 09:36): is what I have to do #### Kevin Buzzard (May 24 2018 at 09:36): which is marking 150 scripts about sup S #### Kevin Buzzard (May 24 2018 at 09:36): I think I need to go offline for 7 hours #### Kevin Buzzard (May 24 2018 at 09:36): I will push too #### Kevin Buzzard (May 24 2018 at 09:37): Before I go #### Kevin Buzzard (May 24 2018 at 09:37): just let me make one thing clear to Kenny and Chris #### Kevin Buzzard (May 24 2018 at 09:37): Last night I was a bit worried about all this #### Kevin Buzzard (May 24 2018 at 09:38): because I still have 10 hours of marking and I wanted to give a good talk on Sat #### Kevin Buzzard (May 24 2018 at 09:38): but now I know I have enough material to give a good talk #### Kevin Buzzard (May 24 2018 at 09:38): so feel free to stop thinking about this and worry about your stats exam #### Kevin Buzzard (May 24 2018 at 09:38): and come back to it on Friday #### Kevin Buzzard (May 24 2018 at 09:38): I will be at Xena tonight by the way, from 6pm #### Kevin Buzzard (May 24 2018 at 09:39): Thanks to all of you, as ever #### Kenny Lau (May 24 2018 at 09:42): lemma nat.mod_rec (m n : ℕ) {C : ℕ → Sort*} (H : ∀ n, C n = C (n+m)) : C n = C (n%m) := have H1 : ∀ q r, C (r + m * q) = C r, from λ q, nat.rec_on q (λ r, by rw [mul_zero]; refl)$ λ n ih r,
by rw [mul_succ, ← add_assoc, ← H, ih],
by conv in (C n) { rw [← mod_add_div n m, H1] }


#### Kenny Lau (May 24 2018 at 11:36):

theorem fib_gcd (m : ℕ) : ∀ n, nat.gcd (fib m) (fib n) = fib (nat.gcd m n) :=
[thing that works]


pushed

pushed

#### Kenny Lau (May 24 2018 at 11:49):

i'm going to eat and then revise statistics until tonight

#### Kevin Buzzard (May 26 2018 at 09:53):

What is the prettiest way to prove that there's a positive real number alpha with the property that alpha ^ 2 = alpha + 1?

not to.

#### Kenny Lau (May 26 2018 at 09:53):

(why can't we just use the Zalpha)

#### Kevin Buzzard (May 26 2018 at 09:54):

I would be really interested in an answer to this question before 2000 BST and ideally earlier

#### Kevin Buzzard (May 26 2018 at 09:54):

Kenny I am giving a talk to a bunch of schoolkids

#### Kevin Buzzard (May 26 2018 at 09:54):

I am going to give two talks

#### Mario Carneiro (May 26 2018 at 09:54):

square root, or FTA

#### Kevin Buzzard (May 26 2018 at 09:54):

In the first talk I will ask them to prove to me that alpha exists and I'll see what they come up with.

#### Kevin Buzzard (May 26 2018 at 09:54):

In the second talk I will show them how Lean does it

#### Kevin Buzzard (May 26 2018 at 09:54):

But I want it to look really sexy

IVT works too

#### Kevin Buzzard (May 26 2018 at 09:55):

I want to define a real number alpha as $(1+5^{(1/2)})/2$ or something that looks as close to that as possible

#### Mario Carneiro (May 26 2018 at 09:55):

then use sqrt thm

#### Kevin Buzzard (May 26 2018 at 09:56):

I would like a square root symbol ideally. Is there one of them?

#### Kevin Buzzard (May 26 2018 at 09:56):

Oh I saw one in Pell maybe?

#### Mario Carneiro (May 26 2018 at 09:56):

I thought we did this a few months ago

#### Kevin Buzzard (May 26 2018 at 09:56):

I know how to solve it

#### Kevin Buzzard (May 26 2018 at 09:56):

I just want to make it look maximally sexy

#### Kevin Buzzard (May 26 2018 at 09:57):

I want to write a human-readable proof

#### Mario Carneiro (May 26 2018 at 09:57):

I think it is \surd

it is in pell

#### Kevin Buzzard (May 26 2018 at 09:58):

i.e. something where you show the exact proof to a smart schoolkid and whilst they don't know any of the precise syntax they can still kind of see that it's a proof that if alpha is (1+sqrt(5))/2 then alpha^2=alpha+1.

#### Kevin Buzzard (May 26 2018 at 09:58):

I'll see what I can come up with

#### Kevin Buzzard (May 26 2018 at 10:00):

I fear becoming mired in div_muls and mul_adds when expanding everything out

#### Mario Carneiro (May 26 2018 at 10:00):

complete the square

using ring

#### Kevin Buzzard (May 26 2018 at 13:30):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by norm_num -- fails

#### Kevin Buzzard (May 26 2018 at 13:30):

Why can't it be easy

#### Kevin Buzzard (May 26 2018 at 13:30):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [(sqrt_prop 5).2] -- fails

#### Kevin Buzzard (May 26 2018 at 13:30):

I am so bad at reals

#### Kevin Buzzard (May 26 2018 at 13:30):

#check sqrt_prop -- ∀ (x : ℝ), 0 ≤ sqrt x ∧ sqrt x * sqrt x = max 0 x

#### Mario Carneiro (May 26 2018 at 13:32):

you want sqr_sqrt

#### Mario Carneiro (May 26 2018 at 13:32):

it's already a simp lemma, so you just have to supply a proof of 0 <= 5

#### Kevin Buzzard (May 26 2018 at 13:32):

why do I need to supply a proof of that?

#### Kevin Buzzard (May 26 2018 at 13:32):

It's clear it will yield to norm_num right?

#### Kevin Buzzard (May 26 2018 at 13:33):

Can I somehow add norm_num to simp?

#### Mario Carneiro (May 26 2018 at 13:33):

sure, but norm_num and simp don't talk back and forth like that

#### Kevin Buzzard (May 26 2018 at 13:33):

I am still a million miles away from writing a clear readable statement and proof that if alpha = (1+sqrt(5))/2 then alpha^2=alpha+1

#### Kevin Buzzard (May 26 2018 at 13:33):

I will keep trying

#### Mario Carneiro (May 26 2018 at 13:34):

norm_num doesn't know about square roots, and simp doesn't use norm_num as a discharger

#### Mario Carneiro (May 26 2018 at 13:34):

you could try simp {discharger := norm_num}, not sure if that works

#### Kevin Buzzard (May 26 2018 at 13:34):

completely unrelated -- why do I have imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/set/lattice.lean' uses sorry and several other mathlib errors? This looks really unprofessional :-/ Can you tell me a quick fix?

#### Mario Carneiro (May 26 2018 at 13:34):

still, I think simp (dec_trivial : 0 <= 5) is easy enough

#### Kevin Buzzard (May 26 2018 at 13:35):

That's enough? It goes from nats to reals?

#### Mario Carneiro (May 26 2018 at 13:35):

Oh wait no, le on real is not computable

#### Mario Carneiro (May 26 2018 at 13:35):

you need to use norm_num

#### Mario Carneiro (May 26 2018 at 13:35):

simp [(by norm_num : 0 <= 5)]

#### Kevin Buzzard (May 26 2018 at 13:36):

I don't understand what you are saying

#### Kevin Buzzard (May 26 2018 at 13:36):

I don't understand this stuff well enough

#### Kevin Buzzard (May 26 2018 at 13:36):

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,(dec_trivial : 0 <= 5)]-- fails

#### Kevin Buzzard (May 26 2018 at 13:36):

I am not even sure that's valid syntax

it should be...

#### Mario Carneiro (May 26 2018 at 13:37):

the full proof is just sqr_sqrt (by norm_num : 0 <= 5)

#### Kevin Buzzard (May 26 2018 at 13:38):

theorem zero_le_5 : (0 : ℝ) ≤ 5 := by norm_num

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,zero_le_5]


#### Kevin Buzzard (May 26 2018 at 13:38):

First molehill conquered

#### Mario Carneiro (May 26 2018 at 13:38):

Oh, you might need to write simp [(by norm_num : (0:R) <= 5)]

Where?

#### Mario Carneiro (May 26 2018 at 13:39):

as a proof of the theorem

#### Mario Carneiro (May 26 2018 at 13:39):

that proves zero_le_5 inline, and uses it as a simp lemma in the main proof

#### Kevin Buzzard (May 26 2018 at 13:40):

It's really annoying to use Lean like this. Why do I have all these errors in mathlib?

#### Kevin Buzzard (May 26 2018 at 13:40):

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/bounded_lattice.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/finset.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/boolean_algebra.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/equiv.lean' uses sorry
real_alpha.lean:1:0: warning

imported file '/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/data/set/lattice.lean' uses sorry


#### Kevin Buzzard (May 26 2018 at 13:40):

What have I done wrong?

#### Mario Carneiro (May 26 2018 at 13:41):

maybe those files use sorry

#### Kevin Buzzard (May 26 2018 at 13:41):

I thought I was all up to date

#### Mario Carneiro (May 26 2018 at 13:41):

Look for an actual error

#### Mario Carneiro (May 26 2018 at 13:42):

Usually lean will have some error in a theorem, and then since the theorem failed it uses sorry instead, and then every other file that imports that file complains about the sorry so you get hundreds of sorry warnings

#### Kevin Buzzard (May 26 2018 at 13:42):

complete_lattice.lean:119:36: error

⊥
⊥
/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean:119:36: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
?m_1
the following overloaded terms were applicable
⊥
⊥


#### Kevin Buzzard (May 26 2018 at 13:43):

Looks like much of a muchness to me

#### Kevin Buzzard (May 26 2018 at 13:44):

don't know how to synthesize placeholder
context:
α : Type u,
_inst_1 : lattice.complete_lattice.{u} α
⊢ Type ?l_1
complete_lattice.lean:120:36: error

@lattice.has_bot.bot.{?l_1} ?m_2 ?m_3
@lattice.has_bot.bot.{?l_4} ?m_5 ?m_6
/home/buzzard/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib/order/complete_lattice.lean:120:36: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
?m_1
the following overloaded terms were applicable
@lattice.has_bot.bot.{?l_2} ?m_3 ?m_4
@lattice.has_bot.bot.{?l_5} ?m_6 ?m_7


with pp_all on

#### Mario Carneiro (May 26 2018 at 13:44):

what about #print ⊥?

#### Kevin Buzzard (May 26 2018 at 13:45):

⊥:1024 :=
| lattice.has_bot.bot _
| lattice.has_bot.bot _


#### Mario Carneiro (May 26 2018 at 13:45):

some file somewhere has declared ⊥ as a global notation

Thanks

#### Mario Carneiro (May 26 2018 at 13:45):

I recently moved the location of the declaration of ⊥

#### Mario Carneiro (May 26 2018 at 13:46):

it's possible you have an old version of one of the files and so are getting a double declaration

Thanks

#### Kevin Buzzard (May 26 2018 at 13:46):

I can't see any of these symbols or bot in my file

#### Mario Carneiro (May 26 2018 at 13:46):

check lattice.lean

:~/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib$git branch * (HEAD detached at 6811f13) master  #### Kevin Buzzard (May 26 2018 at 13:47): I don't know what detached head means #### Mario Carneiro (May 26 2018 at 13:47): or just search for notation ⊥  #### Kevin Buzzard (May 26 2018 at 13:47): Should I switch to master? #### Mario Carneiro (May 26 2018 at 13:47): it means you have a commit checked out, not a branch #### Mario Carneiro (May 26 2018 at 13:48): what does git status give? #### Kevin Buzzard (May 26 2018 at 13:48): That sounds right #### Kevin Buzzard (May 26 2018 at 13:48): shall I checkout a branch? #### Kevin Buzzard (May 26 2018 at 13:48): I did everything with leanpkg as far as I know #### Mario Carneiro (May 26 2018 at 13:49): leanpkg usually checks out commits, which is why it is like that #### Kevin Buzzard (May 26 2018 at 13:49): $ git status
nothing to commit, working directory clean


#### Kevin Buzzard (May 26 2018 at 13:49):

can you just tell me how to install the latest mathlib and get it all working?

#### Mario Carneiro (May 26 2018 at 13:50):

You appear to have it already, from that status message

#### Kevin Buzzard (May 26 2018 at 13:50):

Is there just a brutal fix so I have a working version of mathlib? Should I just delete _target and run leanpkg something?

#### Kevin Buzzard (May 26 2018 at 13:50):

Or check out some other commit or branch?

#### Kevin Buzzard (May 26 2018 at 13:51):

I just want to get this fixed quickly, I am giving a talk in an hour

#### Mario Carneiro (May 26 2018 at 13:51):

yes probably, but I'm not a leanpkg expert

#### Kevin Buzzard (May 26 2018 at 13:51):

and then another one at 8 where I want to show Lean off

#### Kevin Buzzard (May 26 2018 at 13:51):

and all its erros

errors

#### Mario Carneiro (May 26 2018 at 13:51):

maybe back up the directory first, but sure just remove _target and do the usual leanpkg incantations

#### Mario Carneiro (May 26 2018 at 13:52):

that folder only has cached stuff so it should be fine

#### Kevin Buzzard (May 26 2018 at 13:52):

I'm on a train :-/

#### Mario Carneiro (May 26 2018 at 13:53):

try removing .olean files

and rebuild

#### Mario Carneiro (May 26 2018 at 13:54):

did you search for notation bot like I said?

git is working

really good

#### Kevin Buzzard (May 26 2018 at 13:54):

patchy 3g phone and hotspot

#### Mario Carneiro (May 26 2018 at 13:54):

this line

notation ⊥ := has_bot.bot _


should appear exactly once in mathlib, in bounded_lattice.lean

#### Kevin Buzzard (May 26 2018 at 13:55):

I got bored trying to work out why it was broken

#### Kevin Buzzard (May 26 2018 at 13:55):

I am under time pressure

#### Mario Carneiro (May 26 2018 at 13:55):

I'm hoping that the location of the second hit will hint at why you have old files

#### Mario Carneiro (May 26 2018 at 13:56):

that's why I'm giving suggestions that are fast to check

#### Kevin Buzzard (May 26 2018 at 13:58):

you could try simp {discharger := norm_num}, not sure if that works

I can't get it to work

#### Chris Hughes (May 26 2018 at 13:59):

example : (((1 : ℝ) + √5) / 2) ^ 2 = ((1 : ℝ) + √5 ) / 2 + 1 :=
have h : (0 : ℝ) ≤ 5 := by norm_num,
begin
ring,
end


#### Kevin Buzzard (May 26 2018 at 13:59):

import analysis.real tactic.norm_num tactic.ring

namespace real
noncomputable theory

def α := (real.sqrt 5 + 1) / 2
def β := 1 - α

theorem root_5_squared : (sqrt 5) ^ 2 = 5 := by simp [sqr_sqrt,(by norm_num : (0:ℝ) <= 5)]

lemma αβsum : α + β = 1 := begin
unfold β,
unfold α,
norm_num, -- ;-)
end

lemma αβprod : α * β = -1 := begin
unfold β,
unfold α,
simp [root_5_squared],
norm_num, -- unknown exception while type-checking theorem
end


#### Kevin Buzzard (May 26 2018 at 13:59):

I got an achievement -- "unknown exception while type-checking theorem"

#### Kevin Buzzard (May 26 2018 at 14:00):

Why isn't this easy

#### Kevin Buzzard (May 26 2018 at 14:00):

simp wants facts from norm_num but I don't know what facts

#### Kevin Buzzard (May 26 2018 at 14:00):

goal after simp is

#### Kevin Buzzard (May 26 2018 at 14:00):

⊢ 2⁻¹ +
(sqrt 5 / 2 +
(-(2⁻¹ * 2⁻¹) + (-(2⁻¹ * (sqrt 5 / 2)) + (-(sqrt 5 / 2 * 2⁻¹) + -(sqrt 5 / 2 * (sqrt 5 / 2)))))) =
-1


#### Kevin Buzzard (May 26 2018 at 14:01):

I must have taken a wrong turn

#### Kevin Buzzard (May 26 2018 at 14:01):

I am not a competent driver when it comes to the reals

#### Mario Carneiro (May 26 2018 at 14:01):

simp on its own will not know how to finish the job

#### Mario Carneiro (May 26 2018 at 14:01):

you need ring for all that

#### Kevin Buzzard (May 26 2018 at 14:02):

All I want to do is prove that if alpha is (1+sqrt(5))/2 then alpha^2=alpha+1

in R

#### Kevin Buzzard (May 26 2018 at 14:02):

because if that's not easy

#### Kevin Buzzard (May 26 2018 at 14:02):

then what kind of an R have you got here

#### Kevin Buzzard (May 26 2018 at 14:02):

a computer scientist's one but not a mathematican's one

#### Kevin Buzzard (May 26 2018 at 14:03):

I completely understand the other approach

#### Kevin Buzzard (May 26 2018 at 14:03):

but for pedagogical reasons I would like to see this happening in R

#### Kevin Buzzard (May 26 2018 at 14:03):

I can always fall back on Nicholas' construction

#### Kevin Buzzard (May 26 2018 at 14:03):

which indeed I will ultimately fall back on

#### Kevin Buzzard (May 26 2018 at 14:04):

but my goal was not to explain how incredibly difficult it was to even the most trivial things

I get it

1 sec

Sorry to moan

#### Kevin Buzzard (May 26 2018 at 14:04):

I am giving an important talk

#### Kevin Buzzard (May 26 2018 at 14:05):

and I want it to be _really good_

#### Mario Carneiro (May 26 2018 at 14:05):

I believe it can be done with a short tactic invoke

#### Kevin Buzzard (May 26 2018 at 14:05):

so I want to make a really professional job of it

#### Mario Carneiro (May 26 2018 at 14:05):

I think you can use ring to get it down to an expression involving (sqrt 5)^2, and then use simp and norm_num to finish

#### Kevin Buzzard (May 26 2018 at 14:07):

Removed target and re-installed everything and I'm back up to speed :-)

#### Kevin Buzzard (May 26 2018 at 14:07):

one further step towards professional

No more errors

#### Kevin Buzzard (May 26 2018 at 14:08):

aargh that's a lie

#### Kevin Buzzard (May 26 2018 at 14:09):

I will sort this out later -- I've got until 8pm

#### Mario Carneiro (May 26 2018 at 14:09):

what time is it now?

#### Kenny Lau (May 26 2018 at 14:09):

I will sort this out later -- I've got until 8pm

what do you need to sort out?

#### Kevin Buzzard (May 26 2018 at 14:10):

I have loads of errors in mathlib

#### Kevin Buzzard (May 26 2018 at 14:10):

I've tried everything

#### Kevin Buzzard (May 26 2018 at 14:10):

I might reboot my computer

#### Kevin Buzzard (May 26 2018 at 14:10):

and recompile all .olean files

#### Kenny Lau (May 26 2018 at 14:10):

are you trying to prove anything?

#### Kevin Buzzard (May 26 2018 at 14:10):

but that's all I can think of

#### Kevin Buzzard (May 26 2018 at 14:11):

I'm tyring to prove that two real numbers are equal

I'll push

#### Kevin Buzzard (May 26 2018 at 14:12):

https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/real_alpha.lean

#### Kevin Buzzard (May 26 2018 at 14:12):

But I want it to look sexy

#### Mario Carneiro (May 26 2018 at 14:13):

you could import data.real.basic instead

#### Mario Carneiro (May 26 2018 at 14:22):

import data.real.basic tactic.norm_num tactic.ring

open real
noncomputable theory

prefix √:90 := sqrt

def α := (√5 + 1) / 2
def β := 1 - α

theorem root_5_squared : √5 ^ 2 = 5 :=
by simp {discharger := [norm_num]}

lemma αβsum : α + β = 1 := begin
unfold α β,
ring
end

lemma αβprod : α * β = -1 := begin
unfold α β,
ring,
simp {discharger := [norm_num]},
ring
end


what

#### Kenny Lau (May 26 2018 at 14:27):

import data.real.basic tactic.norm_num

noncomputable theory

prefix √:90 := real.sqrt

def α := (1 + √5) / 2
def β := 1 - α

theorem root_5_squared : √5 * √5 = 5 :=
real.mul_self_sqrt $show (0:ℝ) ≤ 5, by norm_num lemma αβsum : α + β = 1 := show α + (1 - α) = 1, from add_sub_cancel'_right α 1 lemma αβprod : α * β = -1 := calc α * β = ((1 + √5) / 2) * (1 - (1 + √5) / 2) : rfl ... = ((1 + √5) / 2) * ((1 + 1) / 2 - (1 + √5) / 2) : by rw add_self_div_two ... = ((1 + √5) / 2) * (((1 + 1) - (1 + √5)) / 2) : by rw div_sub_div_same ... = ((1 + √5) / 2) * ((1 - √5) / 2) : by rw add_sub_add_left_eq_sub ... = ((1 + √5) * (1 - √5)) / (2 * 2) : by rw div_mul_div ... = (1 * 1 - √5 * √5) / (2 * 2) : by rw mul_self_sub_mul_self_eq ... = (1 * 1 - 5) / (2 * 2) : by rw root_5_squared ... = -1 : by norm_num  #### Kenny Lau (May 26 2018 at 14:27): @Kevin Buzzard do you like direct proofs? #### Mario Carneiro (May 26 2018 at 14:28): You could also half-cheat and write a plausible-looking sequence of equalities all proven by ring #### Kenny Lau (May 26 2018 at 14:28): but that defeats the purpose of the presentation #### Kevin Buzzard (May 26 2018 at 14:28): This is somehow awful #### Mario Carneiro (May 26 2018 at 14:28): it makes it look nice and readable #### Kevin Buzzard (May 26 2018 at 14:28): but it's much better than nothing #### Kevin Buzzard (May 26 2018 at 14:28): But I don't want it to be readable #### Kevin Buzzard (May 26 2018 at 14:28): I want it to be trivial #### Kenny Lau (May 26 2018 at 14:28): what #### Kevin Buzzard (May 26 2018 at 14:28): An obscure one-liner? #### Mario Carneiro (May 26 2018 at 14:28): you didn't like my ring solution? #### Kenny Lau (May 26 2018 at 14:29): I thought you're teaching rigour #### Kenny Lau (May 26 2018 at 14:29): if you asked me in m1f to prove that alpha * beta = -1, that is exactly what I would write down #### Kenny Lau (May 26 2018 at 14:29): minus the by rw ... things #### Kevin Buzzard (May 26 2018 at 14:29): I don't understand -- what ring solution? #### Kenny Lau (May 26 2018 at 14:29): https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Largest.20Square.20in.20the.20Fibonacci.20Sequence/near/127129776 #### Kenny Lau (May 26 2018 at 14:29): :D #### Kenny Lau (May 26 2018 at 14:30): I can't delete my own messages... #### Kevin Buzzard (May 26 2018 at 14:30): I want as many solutions as I can #### Kevin Buzzard (May 26 2018 at 14:31): And we vote for the most beautiful #### Kenny Lau (May 26 2018 at 14:31): beauty is in the eye of the beholder #### Kenny Lau (May 26 2018 at 14:31): in this case, you #### Kenny Lau (May 26 2018 at 14:31): it's you who is/are presenting #### Mario Carneiro (May 26 2018 at 14:33): semi-explicit, only one ring lemma αβprod : α * β = -1 := begin unfold α β, ring, rw sqr_sqrt; norm_num end  #### Kenny Lau (May 26 2018 at 14:33): I still don't know what @Kevin Buzzard wants #### Kenny Lau (May 26 2018 at 14:33): what is the goal of this? #### Reid Barton (May 26 2018 at 14:36): or an intermediate one, still using calc lemma αβsum : α + β = 1 := by dsimp [β]; ring lemma αβprod : α * β = -1 := calc α * β = ((1 + √5) / 2) * (1 - (1 + √5) / 2) : rfl ... = (1 * 1 - √5^2) / (2 * 2) : by ring ... = -1 : by rw real.sqr_sqrt; norm_num  #### Mario Carneiro (May 26 2018 at 14:37): I guess you could write the middle line as (1 - √5^2) / 4 for extra clean #### Kenny Lau (May 26 2018 at 14:37): low-tech one-liners: #### Kenny Lau (May 26 2018 at 14:37): import data.real.basic tactic.norm_num noncomputable theory prefix √:90 := real.sqrt def α := (1 + √5) / 2 def β := (1 - √5) / 2 theorem root_5_squared : √5 * √5 = 5 := real.mul_self_sqrt$ show (0:ℝ) ≤ 5, by norm_num

lemma αβsum : α + β = 1 :=
by rw [α, β, ← add_div]; simp

lemma αβprod : α * β = -1 :=
by rw [α, β, div_mul_div, ← mul_self_sub_mul_self_eq, root_5_squared]; norm_num


#### Kenny Lau (May 26 2018 at 14:38):

(is changing the definition allowed?)

#### Mario Carneiro (May 26 2018 at 14:40):

lemma αβprod : α * β = -1 :=
calc ((√5 + 1) / 2) * (1 - (√5 + 1) / 2)
= (1 - √5^2) / 4 : by ring
... = -1 : by rw sqr_sqrt; norm_num


#### Kenny Lau (May 26 2018 at 14:40):

not very different from the one above...

#### Mario Carneiro (May 26 2018 at 14:41):

it's based on reid's

#### Kenny Lau (May 26 2018 at 14:42):

import data.real.basic tactic.norm_num

noncomputable theory

prefix √:90 := real.sqrt

def α := (1 + √5) / 2
def β := (1 - √5) / 2

lemma sqrt_5_mul_self : √5 * √5 = 5 :=
real.mul_self_sqrt $show (0:ℝ) ≤ 5, by norm_num lemma αβsum : α + β = 1 := by simp [α, β, add_div, neg_div, -one_div_eq_inv] lemma αβprod : α * β = -1 := by simp [α, β, div_mul_div, add_mul, mul_add, sqrt_5_mul_self]; norm_num  #### Reid Barton (May 26 2018 at 14:42): And I just took Kenny's long calc and deleted all the intermediate steps that could be handled by ring. #### Reid Barton (May 26 2018 at 14:43): I like calc here because the fact α * β = -1 is actually not immediately obvious to a human, and you'd write out about the same number of intermediate steps to explain the calculation to a human. #### Kenny Lau (May 26 2018 at 14:43): still avoiding ring as usual :P #### Kenny Lau (May 26 2018 at 14:44): I like my new definition #### Kenny Lau (May 26 2018 at 14:44): who likes my new definition #### Mario Carneiro (May 26 2018 at 14:44): I think your definition is nicer if you are going to define both alpha and beta #### Mario Carneiro (May 26 2018 at 14:45): In a human proof I would probably have an additional step in the middle with all four terms and cross out the cross terms #### Kenny Lau (May 26 2018 at 14:46): that's what I did with the add_mul and mul_add #### Kenny Lau (May 26 2018 at 14:46): import data.real.basic tactic.norm_num noncomputable theory prefix √:90 := real.sqrt def α := (1 + √5) / 2 def β := (1 - √5) / 2 lemma sqrt_5_mul_self : √5 * √5 = 5 := real.mul_self_sqrt$ show (0:ℝ) ≤ 5, by norm_num1

lemma αβsum : α + β = 1 :=
by simp [α, β, add_div, neg_div, -one_div_eq_inv]

lemma αβprod : α * β = -1 :=


low-tech :P

#### Mario Carneiro (May 26 2018 at 14:46):

A long rw proof is hard to read though

#### Mario Carneiro (May 26 2018 at 14:47):

unless you step through it

#### Kenny Lau (May 26 2018 at 14:47):

I thought @Kevin Buzzard wants a one-liner

#### Mario Carneiro (May 26 2018 at 14:47):

and you can't even do that for a simp proof

#### Mario Carneiro (May 26 2018 at 14:47):

I think we have that already

#### Mario Carneiro (May 26 2018 at 14:48):

lemma αβprod : α * β = -1 :=
by unfold α β; ring; simp {discharger := [norm_num]}; ring


#### Mario Carneiro (May 26 2018 at 14:51):

ooh, with this modification to norm_num:

meta def norm_num (loc : parse location) : tactic unit :=
let t := orelse' (norm_num1 loc) \$
simp_core {} (norm_num1 (interactive.loc.ns [none])) ff [] [] loc in
t >> repeat t


you can get away with just by unfold α β; ring; norm_num

#### Kevin Buzzard (May 26 2018 at 15:01):

I just want to explain to kids who don't know any better, what maths is

#### Kenny Lau (May 26 2018 at 15:02):

then why wouldn't you write down every step

#### Kevin Buzzard (May 26 2018 at 15:02):

All of this stuff is great

#### Kevin Buzzard (May 26 2018 at 15:02):

Because what is a step when you are 16 years old?

#### Kevin Buzzard (May 26 2018 at 15:02):

You have never thought about steps

#### Mario Carneiro (May 26 2018 at 15:03):

I presume that will be part of the talk

#### Mario Carneiro (May 26 2018 at 15:03):

at least, the idea that math is built on axioms and rules

#### Mario Carneiro (May 26 2018 at 15:03):

and you have to use those rules to prove things

#### Mario Carneiro (May 26 2018 at 15:03):

the sense of "step" is not far from this

Yes exactly

#### Kevin Buzzard (May 26 2018 at 15:09):

I will be here at 8pm UK time (i.e. now + 3h50m) asking more stupid questions about real numbers

#### Nicholas Scheel (May 26 2018 at 16:37):

lemma α_sqr : α^2 = α + 1 := rfl in ℤα ;)

#### Kenny Lau (May 26 2018 at 16:37):

but he doesn't want to use Zalpha in the presentation lol

#### Nicholas Scheel (May 26 2018 at 16:38):

btw I proved point 3, should I leave it in Zalpha or move it to a point3.lean?

#### Kenny Lau (May 26 2018 at 16:38):

move it to point3.lean

done!

#### Nicholas Scheel (May 26 2018 at 16:43):

I tried and failed to prove that it is an integral domain, got any tips?

#### Kenny Lau (May 26 2018 at 16:44):

where are you stuck in?

#### Nicholas Scheel (May 26 2018 at 16:49):

it’s something like
a * c + b * d = 0 AND a * d + b * c + b * d = 0 IMPLIES THAT (a, b) = 0 OR (c, d) = 0

#### Nicholas Scheel (May 26 2018 at 16:52):

I understand that it’s equivalent to the fact that α is not an integer, and equivalent to the fact that 1 and α are linearly independent, but I don’t see how to do that from the definition of multiplication

#### Johan Commelin (May 26 2018 at 17:08):

Well, you could define an embedding of Zalpha into R.

#### Johan Commelin (May 26 2018 at 17:09):

I think we now have about a dozen proofs of why that works :wink:

#### Kenny Lau (May 26 2018 at 17:09):

proving that it is injective needs work also

#### Johan Commelin (May 26 2018 at 17:10):

That is the linear independence of 1 and alpha

sure, why not ;D

#### Kenny Lau (May 26 2018 at 17:15):

oh right you need to prove that sqrt(5) is irrational

#### Kevin Buzzard (May 26 2018 at 21:09):

Yeah, that's the analogue of showing that if $z=x+iy$ is a complex number which isn't zero, then you can divide by $z$, by multiplying by $\overline{z}$ and then dividing by the non-zero real $z\overline{z}$.

#### Kevin Buzzard (May 26 2018 at 21:10):

In this instance it boils down to proving that the product of $a+b\surd{5}$ and its Galois conjugate $a-b\surd{5}$ is non-zero if at least one of $a$ and $b$ is non-zero

#### Kevin Buzzard (May 26 2018 at 21:10):

\surdfor square roots in maths mode, not \sqrt

#### Kevin Buzzard (May 26 2018 at 21:10):

So as Kenny says it's precisely the irrationality of $\surd 5$, or, more precisely, it's the statement that no rational number squared is $5$ (rather than any statement about real numbers not being rational)

#### Kevin Buzzard (May 26 2018 at 21:10):

So one way to do it is to prove that if $a+b\surd 5$ is non-zero then the rational $a^2-5b^2$ is non-zero and then use that a non-zero rational has an inverse.

#### Kevin Buzzard (May 26 2018 at 21:15):

I've just been telling some kids about Lean. Some of them got into it. We were doing induction on nat and on or and on false and stuff

#### Kevin Buzzard (May 26 2018 at 21:15):

I did some Fibonacci stuff

#### Kevin Buzzard (May 26 2018 at 21:15):

and some logic stuff

#### Kevin Buzzard (May 26 2018 at 21:15):

and we looked at why induction was a theorem in Lean

#### Nicholas Scheel (May 26 2018 at 21:28):

Well, you could define an embedding of Zalpha into R.

Thanks @Johan Commelin I think that worked ;) https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/Zalpha_real.lean
again, ugly code, but it typechecks

#### Nicholas Scheel (May 26 2018 at 21:36):

and thanks @Chris Hughes for the alpha squared proof, such a time saver! :D

#### Kenny Lau (May 26 2018 at 22:41):

hmm, I wonder if we can shorten it

#### Kenny Lau (May 26 2018 at 22:58):

@Nicholas Scheel do you mind if I edit your files?

go for it!

#### Nicholas Scheel (May 26 2018 at 22:58):

I think I’m done for now, have to spend time on other things now

#### Nicholas Scheel (May 26 2018 at 22:59):

but I’m curious: what is norm_num? I haven’t found much documentation for it

#### Kevin Buzzard (May 26 2018 at 23:03):

It proves identities between explicit real numbers

#### Kevin Buzzard (May 26 2018 at 23:03):

And inequalities etc

#### Nicholas Scheel (May 26 2018 at 23:05):

cool :simple_smile:

#### Kenny Lau (May 26 2018 at 23:16):

theorem α_fib (n : ℕ) : α^(n+1) = ⟨Fib n, Fib (n+1)⟩ :=
begin
induction n with n ih, { refl },
change α*α^(n + 1) = ⟨Fib (n+1), Fib (n+2)⟩,
rw ih, apply ext; simp [-add_comm],
exact int.coe_nat_inj'.2 rfl
end


#### Kenny Lau (May 26 2018 at 23:16):

I golfed off a lot of lines from here

#### Nicholas Scheel (May 26 2018 at 23:18):

that’s great :smiley:

#### Kenny Lau (May 26 2018 at 23:20):

theorem α_fib (n : ℕ) : α^(n+1) = ⟨Fib n, Fib (n+1)⟩ :=
begin
induction n with n ih, { refl },
change α*α^(n + 1) = ⟨Fib (n+1), Fib (n+2)⟩,
rw ih, apply ext; simp [-add_comm, Fib.is_fib]
end


#### Nicholas Scheel (May 26 2018 at 23:22):

🤯 change sounds amazing, funny that I hadn’t run across it before

#### Kenny Lau (May 26 2018 at 23:23):

do you realize that the show in tactic mode is different from the show in term mode

#### Kenny Lau (May 26 2018 at 23:23):

and then change is a generalization of that, that allows you to change the hypotheses as well

#### Nicholas Scheel (May 26 2018 at 23:29):

I haven’t used show in term mode, what’s the difference?

#### Kenny Lau (May 26 2018 at 23:30):

well there's not a huge difference

#### Reid Barton (May 26 2018 at 23:38):

I haven't used show in tactic mode!

#### Nicholas Scheel (May 26 2018 at 23:39):

that moment when computer programs understand analogies better than we expect :wink:

#### Kenny Lau (May 27 2018 at 01:27):

@Nicholas Scheel I hope you don't mind

#### Kenny Lau (May 27 2018 at 01:28):

https://github.com/kbuzzard/lean-squares-in-fibonacci/commit/7ba981070187c25d322b0e8de14021ec7214ddb9#diff-44f4839567c6f9e6617b4e04801b926a

#### Kenny Lau (May 27 2018 at 01:33):

TODO: incorporate this

#### Nicholas Scheel (May 27 2018 at 01:42):

not at all, that’s cool! thanks!

#### Kenny Lau (May 27 2018 at 02:00):

https://github.com/kbuzzard/lean-squares-in-fibonacci/commit/9106996916442e8f17239323d5a6cbe3e236efd3#diff-44f4839567c6f9e6617b4e04801b926a

done

#### Chris Hughes (May 27 2018 at 11:56):

I'm working on polys. I've just done the remainder theorem.

#### Kevin Buzzard (May 27 2018 at 12:01):

Polys in 1 variable need to go in mathlib so perhaps keep this in mind

#### Kevin Buzzard (May 27 2018 at 12:02):

When I write code now, I realise that sometimes it's code for me and sometimes it's stuff I think should be in mathlib

#### Kevin Buzzard (May 27 2018 at 12:02):

And I've started separating the two

#### Kevin Buzzard (May 27 2018 at 12:09):

I think this is an interesting consequence of proving "random" things like 144 being the largest square in the Fibonacci sequence.

#### Kevin Buzzard (May 27 2018 at 12:10):

I am pretty sure (am I right @Mario Carneiro ?) that mathlib has no interest in keeping and maintaining a proof of the curiosity that 144 is the largest square in the Fibonacci sequence.

However

#### Kevin Buzzard (May 27 2018 at 12:11):

When a mathematician looks at the proof, they expect to have to work in some areas

#### Kevin Buzzard (May 27 2018 at 12:11):

but conversely they expect some "standard tools" to be there

#### Kevin Buzzard (May 27 2018 at 12:11):

and this can be used to guide development of mathlib

#### Kevin Buzzard (May 27 2018 at 12:11):

For example, at some point someone is going to need quadratic reciprocity

#### Kevin Buzzard (May 27 2018 at 12:12):

and we will end up developing some of the tools needed to prove QR in this 144 proof

#### Kevin Buzzard (May 27 2018 at 12:12):

and I think there's a strong argument for QR going into mathlib as it's one of the jewels in the crown of mathematics

#### Kevin Buzzard (May 27 2018 at 12:13):

[as well as being a special case of Langlands Reciprocity ;-) ]

#### Kevin Buzzard (May 27 2018 at 12:13):

In the 144 proof we don't need full QR

#### Kevin Buzzard (May 27 2018 at 12:13):

but we need Gauss' Lemma and Euler's Criterion

#### Kevin Buzzard (May 27 2018 at 12:14):

so we're starting along the road to QR with these.

#### Kenny Lau (May 27 2018 at 12:29):

instance : decidable_linear_ordered_comm_ring ℤα :=


#### Kenny Lau (May 27 2018 at 12:29):

https://github.com/kbuzzard/lean-squares-in-fibonacci/blob/master/src/Zalpha_Zsqrt5.lean#L38

#### Kenny Lau (May 27 2018 at 12:29):

@Nicholas Scheel @Kevin Buzzard I find embedding into ℤ√5 a better idea than embedding into the reals

#### Kevin Buzzard (May 27 2018 at 12:43):

Mario's $\mathbb{Z}[\surd{5}]$?

#### Kevin Buzzard (May 27 2018 at 12:43):

(why doesn't sqrt work in LaTeX?)

#### Kevin Buzzard (May 27 2018 at 12:43):

He proved it was an ID?

#### Kenny Lau (May 27 2018 at 12:45):

He proved it was an ID?

yes

#### Kenny Lau (May 27 2018 at 12:45):

(althought I didn't use that)

#### Kenny Lau (May 27 2018 at 12:45):

(I used norm to prove that Zalpha is ID)

#### Kevin Buzzard (May 27 2018 at 12:45):

So how do you deduce ID from norm? You need that if norm is 0 then term is 0, right?

yes

#### Kenny Lau (May 27 2018 at 12:46):

which is tantamount to proving that sqrt5 is irrational

#### Kevin Buzzard (May 27 2018 at 12:46):

and so you need to prove irrationality#

right

#### Kenny Lau (May 27 2018 at 12:46):

on hindsight I should have used the embedding

#### Kenny Lau (May 27 2018 at 12:46):

but I still want to have the norm

#### Kevin Buzzard (May 27 2018 at 12:46):

I was suggesting that Mario might have done that already

#### Kenny Lau (May 27 2018 at 12:46):

the norm is useful

Sure

sure

#### Kevin Buzzard (May 27 2018 at 12:46):

And your norm commutes with Mario's

#### Kevin Buzzard (May 27 2018 at 12:47):

so you could have deduced your norm result from Mario's

#### Kevin Buzzard (May 27 2018 at 12:47):

and this would have saved you the trouble of proving irrationality of sqrt(5)

#### Kenny Lau (May 27 2018 at 12:47):

you see, in my embedding, I multiply the "real value" by 2

#### Kenny Lau (May 27 2018 at 12:47):

because alpha is not an element of Z[sqrt5]

#### Kenny Lau (May 27 2018 at 12:47):

and this would have saved you the trouble of proving irrationality of sqrt(5)

I know

#### Kenny Lau (May 27 2018 at 12:48):

I'll do it when I finish lunch

#### Kevin Buzzard (May 27 2018 at 12:48):

but I guess it's nice to check it every now and then

#### Nicholas Scheel (May 27 2018 at 12:53):

that’s cool! I’ll have to see how Zsqrt is decidable, I just avoided it because it’s irrational xD

#### Nicholas Scheel (May 27 2018 at 12:55):

oh duh: def sq_le (a c b d : ℕ) : Prop := c*a*a ≤ d*b*b

done

#### Kenny Lau (May 27 2018 at 15:35):

now the long proof that 5 is irrational is gone

#### Kenny Lau (May 27 2018 at 15:50):

theorem char_eq (z : ℤα) (H : z * z - z - 1 = 0) : z = α ∨ z = β :=
have H1 : (z - α) * (z - β) = 0,
by rw [← H, α, β]; ring,
(eq_zero_or_eq_zero_of_mul_eq_zero H1).cases_on
(or.inl ∘ eq_of_sub_eq_zero)
(or.inr ∘ eq_of_sub_eq_zero)


#### Kenny Lau (May 27 2018 at 15:50):

completely pointless theorem

#### Kenny Lau (May 27 2018 at 15:50):

Gal(Zalpha/Z) = C2

#### Mario Carneiro (May 27 2018 at 15:51):

I guess z * z - z - 1 = (z - α) * (z - β) is also a way to prove alpha*beta = -1

sure

#### Kenny Lau (May 27 2018 at 16:24):

theorem gal (f : ℤα → ℤα) [is_ring_hom f] : f = id ∨ f = conj :=


lol I did it

nice!

#### Kevin Buzzard (May 27 2018 at 16:37):

Did you develop any tools for proving polys of degree n have at most n roots?

#### Kenny Lau (May 27 2018 at 17:12):

local notation α := Zalpha.units.α

#eval α^(-3:ℤ) -- -3 +   2α
#eval α^(-2:ℤ) --  2 +  -1α
#eval α^(-1:ℤ) -- -1 +   1α
#eval α^( 0:ℤ) --  1 +   0α
#eval α^( 1:ℤ) --  0 +   1α
#eval α^( 2:ℤ) --  1 +   1α
#eval α^( 3:ℤ) --  1 +   2α
#eval α^(12:ℤ) -- 89 + 144α
`

#### Kenny Lau (May 27 2018 at 17:12):

look at what I did

#### Kenny Lau (May 27 2018 at 17:12):

Did you develop any tools for proving polys of degree n have at most n roots?

I thought Chris is doing that

#### Kenny Lau (May 27 2018 at 18:55):

Theorem (reverse mathematics): you need to use induction to prove that L(n) = F(n) + F(n-3).

#### Kenny Lau (May 27 2018 at 18:58):

and if you define L(n) := F(n) + F(n-3), you would have to use induction to prove other things later

#### Mario Carneiro (May 27 2018 at 19:36):

how are those defined?

#### Mario Carneiro (May 27 2018 at 19:41):

From that plot it looks like it's not even true

#### Mario Carneiro (May 27 2018 at 19:43):

L(3) = 4, F(3)+F(0) = 2

#### Kenny Lau (May 27 2018 at 20:44):

@Mario Carneiro I'm an idiot. L(n) = 2F(n) + F(n-3).

what am i doing

#### Kenny Lau (May 27 2018 at 20:45):

@Kevin Buzzard @Nicholas Scheel should we actually call it Zphi instead of Zalpha?

#### Kenny Lau (May 27 2018 at 20:45):

Wikipedia calls its little brother psi

#### Mario Carneiro (May 27 2018 at 21:36):

that one is true for the continuous extension too

#### Mario Carneiro (May 27 2018 at 21:36):

I call the little brother phi bar

#### Mario Carneiro (May 27 2018 at 21:36):

because it's the conjugate of phi

#### Nicholas Scheel (May 27 2018 at 22:24):

they’re alpha equivalent so I don’t care ;) feel free to rename it

#### Kenny Lau (May 27 2018 at 22:27):

@Kevin Buzzard what do you think?

#### Kenny Lau (May 28 2018 at 00:28):

patchily converted everything to Zalpha