Zulip Chat Archive

Stream: maths

Topic: Largest Square in the Fibonacci Sequence


view this post on Zulip Kevin Buzzard (May 23 2018 at 14:07):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:07):

The proof is elementary but delicate

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

I give talks about this to bright schoolchildren occasionally

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

There is a sketch of the idea

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

I'm giving one such talk on Saturday

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

to the British IMO team

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

one on this

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:08):

and one on...whatever I like

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:09):

The only problem is that today is Wednesday

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:09):

which means that it's only three days to Saturday

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:09):

So I did this

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:09):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:09):

and I will start this evening

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

but if anyone wants to help

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

then I would happily let them join in

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

give them push access, whatever

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

(when -2 is a square mod p)

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:10):

or we prove it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:11):

and that Z/pZ is a field

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:11):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:11):

(3) a bunch of relatively simple arithmetic

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:11):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

I attained my schemes goal

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

it's very easy arithmetic

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

and maybe I will do it all myself

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

but if anyone wants to help

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:12):

this would be greatly appreciated :-)

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:15):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:15):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:16):

;-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 14:16):

OK now back to marking

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 23 2018 at 15:03):

He wants a ring, not a field

view this post on Zulip Patrick Massot (May 23 2018 at 15:03):

And that's what this notation denotes

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:11):

maybe a field is fine :-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:11):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:12):

and then mumble about integral domains

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:13):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:13):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 15:13):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (May 23 2018 at 16:54):

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

view this post on Zulip Nicholas Scheel (May 23 2018 at 16:57):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 23 2018 at 18:25):

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

view this post on Zulip Kenny Lau (May 23 2018 at 18:52):

@Kevin Buzzard have you pushed?

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:56):

pushed what?

view this post on Zulip Kenny Lau (May 23 2018 at 18:56):

fibonacci

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:56):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:57):

What Fibonacci is there for me to push?

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:57):

I have epsilon

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:57):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:57):

I will push some stuff

view this post on Zulip Chris Hughes (May 23 2018 at 19:00):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 19:11):

I pushed some stuff

view this post on Zulip Kevin Buzzard (May 23 2018 at 19:12):

I proved 2/3 of point 4

view this post on Zulip 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)]

view this post on Zulip Patrick Massot (May 23 2018 at 19:55):

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

view this post on Zulip Kenny Lau (May 23 2018 at 19:58):

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

view this post on Zulip Patrick Massot (May 23 2018 at 20:00):

I knew it: edge case

view this post on Zulip 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]

view this post on Zulip Kenny Lau (May 23 2018 at 20:00):

there is no edge case!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:09):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:09):

given that 7 divides both 0 and 0

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:12):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:13):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:14):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:15):

but the sum is only over half of the integers

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:15):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:15):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:15):

and that's how I remember it

view this post on Zulip Patrick Massot (May 23 2018 at 20:16):

And we are surprised formalizing maths is hard...

view this post on Zulip Nicholas Scheel (May 23 2018 at 20:19):

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

view this post on Zulip Kenny Lau (May 23 2018 at 20:19):

do I have commit access?

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:21):

what is the most sensible idea?

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:21):

nobody has commit access except me

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:21):

but I am happy to give it to anybody

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:21):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:21):

I need to know your github usernames I guess

view this post on Zulip Kenny Lau (May 23 2018 at 20:22):

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

view this post on Zulip Patrick Massot (May 23 2018 at 20:22):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:24):

OK Kenny and Nicholas you should have push access

view this post on Zulip Kenny Lau (May 23 2018 at 20:24):

thanks

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:24):

but lemme push some stuff

view this post on Zulip Patrick Massot (May 23 2018 at 20:24):

Constructive madness on the way...

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:24):

I need a job done

view this post on Zulip Patrick Massot (May 23 2018 at 20:25):

Selling your mathematician soul...

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:26):

OK I am pushed

view this post on Zulip Kenny Lau (May 23 2018 at 20:27):

waitttt where did the Z alpha come from

view this post on Zulip Kenny Lau (May 23 2018 at 20:27):

oh Nicholas built it...

view this post on Zulip Kenny Lau (May 23 2018 at 20:27):

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

view this post on Zulip Nicholas Scheel (May 23 2018 at 20:27):

oops sorry, did I step on your push?

view this post on Zulip Kenny Lau (May 23 2018 at 20:28):

no

view this post on Zulip Kenny Lau (May 23 2018 at 20:28):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:28):

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

view this post on Zulip Nicholas Scheel (May 23 2018 at 20:28):

I think this might help along the way ;) :

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:28):

that looks really good

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:29):

it's a little bit better than my method

view this post on Zulip Kenny Lau (May 23 2018 at 20:29):

so, constructivism wins?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:29):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:30):

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

view this post on Zulip Kenny Lau (May 23 2018 at 20:30):

you just need the right lemmas

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:30):

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

view this post on Zulip Kenny Lau (May 23 2018 at 20:30):

like the one I proved that day

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:30):

but then you will end up defining some auxiliary function on Z x Z

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:30):

Let me just read through the proof

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:31):

Of course one might also argue that using sqrt(5) is a _natural_ thing to do

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:31):

which might make it a good thing to do

view this post on Zulip 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

view this post on Zulip 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? ;-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:33):

I will write comments about the proof in the issue

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 23 2018 at 20:56):

@Kevin Buzzard can I push?

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:57):

sure go ahead and push

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:57):

I wrote a more detailed sketch of how to flesh out the argument in the issue

view this post on Zulip Kenny Lau (May 23 2018 at 20:58):

are you sure I have write access?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:58):

Kenny I think I invited you. Did you check your email or did I fail?

view this post on Zulip Kenny Lau (May 23 2018 at 20:59):

oh, I need to accept the invitation

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:59):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 23 2018 at 21:03):

pretty sure that exact theorem is in my formalization

view this post on Zulip Mario Carneiro (May 23 2018 at 21:04):

and you don't need UFD for it

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:05):

well you do need something

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:05):

because it's not true in a general ring

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:05):

well I suppose it depends on what you mean by gcd in a general ring

view this post on Zulip Mario Carneiro (May 23 2018 at 21:05):

you need nat.gcd facts and some induction

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:06):

a bit like the proof of UFD ;-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:06):

[I mean, you need nat.gcd facts and some induction for that too]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:07):

and the weaker version of coprime doesn't cut it

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:07):

oh there are also issues with units

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:07):

-4 and -9 are coprime and their product is a square etc etc

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:08):

so there are issues in general

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 23 2018 at 21:08):

right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 23 2018 at 21:23):

n | 2 implies n <= 2

view this post on Zulip Chris Hughes (May 23 2018 at 21:23):

2 is prime

view this post on Zulip Mario Carneiro (May 23 2018 at 21:23):

alternatively, 2 is prime

view this post on Zulip Kenny Lau (May 23 2018 at 21:23):

oh lol

view this post on Zulip Kenny Lau (May 23 2018 at 21:32):

Point 4 done!

view this post on Zulip 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

view this post on Zulip 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 _),

view this post on Zulip Kenny Lau (May 23 2018 at 22:43):

write x^(n+2) as x^n x^2?

view this post on Zulip Kenny Lau (May 23 2018 at 22:43):

you might find int.induction_on useful

view this post on Zulip Kenny Lau (May 24 2018 at 02:44):

Point 6 done except the last claim

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:39):

OK this is great.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:39):

Looking at what has been already done

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:39):

I already easily have enough material to fill the session.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:39):

So actually the time pressure is over.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:40):

These kids are smart kids (my audience of 8)

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:40):

but the Lean session will last 90 minutes

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:41):

that my talk is already written.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:41):

However I am definitely still interested in finishing the job :-)

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:41):

Here's a question.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:42):

Oh -- before I start -- thanks to Kenny and Nicholas for their contributions!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:43):

The question is how to express the following assertion in Lean

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:43):

We need to compute the Fibonacci sequence mod 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:44):

The theorem is that mod 16 it goes like this:

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:45):

And the proof is "trivial by induction"

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:46):

One issue is what to do the induction on.

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:47):

You could do strong induction on m

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:50):

hmm

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:50):

maybe it's OK

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:52):

Hmm

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:57):

Oh -- or are you just talking about the (a+b)%m lemma?

view this post on Zulip Chris Hughes (May 24 2018 at 07:58):

The definition is just quot.mk \circ fib

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

Chris I'm talking about the input not the output

view this post on Zulip Chris Hughes (May 24 2018 at 07:58):

I'm talking about the mod 16 lemma

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

I can get fib : N -> N / 16 fine

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

But fib : (N / 24) -> N / 16 is less fine

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

what am I saying

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

what has happened to me

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:58):

(Z / 24)

view this post on Zulip Chris Hughes (May 24 2018 at 07:59):

Just do nat \r mod 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:59):

what the hell is N mod 24

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:59):

I understand how to build fib : N -> Z / 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 07:59):

The issue is proving that fib (n + 24) = fib n

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

The only proof I know of that statement is

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

"consider n mod 24"

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

Oh

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

I realised I made a mistake above

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

I am going to edit a bunch of 16s and change them to 24s

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:00):

input mod 24, output mod 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:02):

OK fixed

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:02):

So the issue is proving a = b mod 24 implies fib a = fib b mod 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:02):

hmm

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

this is an idea

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

one can prove fib (n + 24) = fib n mod 16

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

by induction on n

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

and one has to hope that Lean has the firepower to compute fib 24

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

to get the induction started

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

OK so

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:03):

actually

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:04):

one can define fibmod16

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:04):

I see

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:04):

fibmod16 : N -> Z/16

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:04):

then prove that forall n, fibmod16 (n + 24) = fibmod16 n by induction on n

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:04):

and now no firepower needed

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:05):

and now prove fib mod 16 is fibmod16 by induction on n

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:05):

and you're done!

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:05):

This is great!

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:05):

Thanks Chris!

view this post on Zulip 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

view this post on Zulip Chris Hughes (May 24 2018 at 08:06):

induction, bases case rfl, next case unfold 24 times, and hope things simplify

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:08):

Yeah I think you've cracked it. Thanks Chris.

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:08):

Now get back to stats revision ;-)

view this post on Zulip Kenny Lau (May 24 2018 at 09:05):

The correct way is to use the theorem I proved that day :P

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:06):

Kenny

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:06):

your comments are sometimes obscure

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:06):

but "the theorem I proved that day" will take some beating

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:06):

(a%m+b%m)%m=(a+b)%m is horrible

view this post on Zulip 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))) :
  by rw [H1, H2, mul_add, mul_add, mul_add, mul_add]; ac_refl

view this post on Zulip Kenny Lau (May 24 2018 at 09:06):

it's how it's done in proofwiki

view this post on Zulip Kenny Lau (May 24 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:07):

"The correct way"

view this post on Zulip Kenny Lau (May 24 2018 at 09:07):

it's more general

view this post on Zulip Kenny Lau (May 24 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:07):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:08):

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

view this post on Zulip Kenny Lau (May 24 2018 at 09:08):

m = 16?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:08):

Oh yeah!

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:08):

Let's talk about that!

view this post on Zulip Kenny Lau (May 24 2018 at 09:08):

that's a special case lol

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:08):

fib n is coprime to fib (n+1)

view this post on Zulip 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 already proved it

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:08):

by Euclid's algorithm

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:09):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:09):

I am going to work with Z/n

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:09):

Where is this in Lean?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:09):

I currently have

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:10):

as long as it's an abelian group

view this post on Zulip Chris Hughes (May 24 2018 at 09:10):

https://github.com/dorhinj/leanstuff/blob/master/Zmod1.lean I did it.

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:11):

oh so it's not in Lean?

view this post on Zulip Chris Hughes (May 24 2018 at 09:11):

No.

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:11):

I mean mathlib

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:11):

OK

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:11):

I will steal it

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:11):

you only did Z mod 1?

view this post on Zulip Chris Hughes (May 24 2018 at 09:12):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:12):

Oh OK :-)

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:12):

That's a relief

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:12):

I was hoping for Zmod16

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:13):

wow

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:13):

https://github.com/dorhinj/leanstuff

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:13):

you have been pretty productive in the last 16 hours

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:13):

about 50 lean files commited

view this post on Zulip Kenny Lau (May 24 2018 at 09:13):

lol

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:14):

it's Chrislib

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:14):

I like the look of kbuzzard.lean

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:14):

Is that one of my theorems?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:14):

something about modular forms maybe?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:15):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:15):

Ellen is going to formalize my dots and boxes paper

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:22):

and it doesn't appear to be there already

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:23):

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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:23):

:-/

view this post on Zulip 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

view this post on Zulip 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 _ _)

view this post on Zulip Patrick Massot (May 24 2018 at 09:28):

This is becoming slightly creepy

view this post on Zulip Patrick Massot (May 24 2018 at 09:28):

Kevin, what have you created?

view this post on Zulip 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]

view this post on Zulip Kenny Lau (May 24 2018 at 09:31):

done

view this post on Zulip Kenny Lau (May 24 2018 at 09:31):

I don't need the fact that fib m and fib m+1 are coprime

view this post on Zulip Kenny Lau (May 24 2018 at 09:32):

I would need it to prove the converse though

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:34):

or showing them code which the tutors can't understand

view this post on Zulip 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"

view this post on Zulip Kenny Lau (May 24 2018 at 09:34):

pushed

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:34):

Thanks Kenny

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

I need a recursor for %

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

If I have a function F from nat to X

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

and a proof that F (n + 24) = F n

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

then I want a theorem that F n = F (n % 24)

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

Is that a recursor?

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:35):

It's what I want, at any rate

view this post on Zulip Kenny Lau (May 24 2018 at 09:36):

ok a minute

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:36):

what I don't want

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:36):

is what I have to do

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:36):

which is marking 150 scripts about sup S

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:36):

I think I need to go offline for 7 hours

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:36):

I will push too

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:37):

Before I go

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:37):

just let me make one thing clear to Kenny and Chris

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:37):

Last night I was a bit worried about all this

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:38):

but now I know I have enough material to give a good talk

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:38):

so feel free to stop thinking about this and worry about your stats exam

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:38):

and come back to it on Friday

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:38):

I will be at Xena tonight by the way, from 6pm

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:39):

Thanks to all of you, as ever

view this post on Zulip 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] }

view this post on Zulip 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]

view this post on Zulip Kenny Lau (May 24 2018 at 11:36):

pushed

view this post on Zulip Kenny Lau (May 24 2018 at 11:49):

pushed

view this post on Zulip Kenny Lau (May 24 2018 at 11:49):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 26 2018 at 09:53):

not to.

view this post on Zulip Kenny Lau (May 26 2018 at 09:53):

(why can't we just use the Zalpha)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:54):

Kenny I am giving a talk to a bunch of schoolkids

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:54):

I am going to give two talks

view this post on Zulip Mario Carneiro (May 26 2018 at 09:54):

square root, or FTA

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:54):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:54):

But I want it to look really sexy

view this post on Zulip Mario Carneiro (May 26 2018 at 09:55):

IVT works too

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:55):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 09:55):

then use sqrt thm

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:56):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:56):

Oh I saw one in Pell maybe?

view this post on Zulip Mario Carneiro (May 26 2018 at 09:56):

I thought we did this a few months ago

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:56):

I know how to solve it

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:56):

I just want to make it look maximally sexy

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:57):

I want to write a human-readable proof

view this post on Zulip Mario Carneiro (May 26 2018 at 09:57):

I think it is \surd

view this post on Zulip Mario Carneiro (May 26 2018 at 09:57):

it is in pell

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 26 2018 at 09:58):

I'll see what I can come up with

view this post on Zulip Kevin Buzzard (May 26 2018 at 10:00):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 10:00):

complete the square

view this post on Zulip Mario Carneiro (May 26 2018 at 10:01):

using ring

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:30):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:30):

Why can't it be easy

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:30):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:30):

I am so bad at reals

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:30):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:32):

you want sqr_sqrt

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:32):

why do I need to supply a proof of that?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:32):

It's clear it will yield to norm_num right?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:33):

Can I somehow add norm_num to simp?

view this post on Zulip Mario Carneiro (May 26 2018 at 13:33):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:33):

I will keep trying

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:34):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 26 2018 at 13:34):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:35):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:35):

Oh wait no, le on real is not computable

view this post on Zulip Mario Carneiro (May 26 2018 at 13:35):

you need to use norm_num

view this post on Zulip Mario Carneiro (May 26 2018 at 13:35):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:36):

I don't understand what you are saying

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:36):

I don't understand this stuff well enough

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:36):

I am not even sure that's valid syntax

view this post on Zulip Mario Carneiro (May 26 2018 at 13:36):

it should be...

view this post on Zulip Mario Carneiro (May 26 2018 at 13:37):

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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:38):

First molehill conquered

view this post on Zulip Mario Carneiro (May 26 2018 at 13:38):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:38):

Where?

view this post on Zulip Mario Carneiro (May 26 2018 at 13:39):

as a proof of the theorem

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:40):

What have I done wrong?

view this post on Zulip Mario Carneiro (May 26 2018 at 13:41):

maybe those files use sorry

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:41):

I thought I was all up to date

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:41):

They're all your files

view this post on Zulip Mario Carneiro (May 26 2018 at 13:41):

Look for an actual error

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:42):

complete_lattice.lean:119:36: error

ambiguous overload, possible interpretations
  ⊥
  ⊥
Additional information:
/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
  ⊥
  ⊥

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:43):

Looks like much of a muchness to me

view this post on Zulip 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

ambiguous overload, possible interpretations
  @lattice.has_bot.bot.{?l_1} ?m_2 ?m_3
  @lattice.has_bot.bot.{?l_4} ?m_5 ?m_6
Additional information:
/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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:44):

with pp_all on

view this post on Zulip Mario Carneiro (May 26 2018 at 13:44):

what about #print ⊥?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:45):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:45):

some file somewhere has declared ⊥ as a global notation

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:45):

Thanks

view this post on Zulip Mario Carneiro (May 26 2018 at 13:45):

I recently moved the location of the declaration of ⊥

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:46):

Thanks

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:46):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:46):

check lattice.lean

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:47):

:~/lean-projects/lean-squares-in-fibonacci/_target/deps/mathlib$ git branch
* (HEAD detached at 6811f13)
  master

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:47):

I don't know what detached head means

view this post on Zulip Mario Carneiro (May 26 2018 at 13:47):

or just search for notation `⊥`

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:47):

Should I switch to master?

view this post on Zulip Mario Carneiro (May 26 2018 at 13:47):

it means you have a commit checked out, not a branch

view this post on Zulip Mario Carneiro (May 26 2018 at 13:48):

what does git status give?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:48):

That sounds right

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:48):

shall I checkout a branch?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:48):

I did everything with leanpkg as far as I know

view this post on Zulip Mario Carneiro (May 26 2018 at 13:49):

leanpkg usually checks out commits, which is why it is like that

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:49):

$ git status
HEAD detached at 6811f13
nothing to commit, working directory clean

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:49):

Instead of trying to debug

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:49):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:50):

You appear to have it already, from that status message

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:50):

Or check out some other commit or branch?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:51):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:51):

yes probably, but I'm not a leanpkg expert

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:51):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:51):

and all its erros

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:51):

errors

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2018 at 13:52):

that folder only has cached stuff so it should be fine

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:52):

I'm on a train :-/

view this post on Zulip Mario Carneiro (May 26 2018 at 13:53):

try removing .olean files

view this post on Zulip Mario Carneiro (May 26 2018 at 13:53):

and rebuild

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:53):

i did that already

view this post on Zulip Mario Carneiro (May 26 2018 at 13:54):

did you search for notation bot like I said?

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:54):

git is working

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:54):

really good

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:54):

patchy 3g phone and hotspot

view this post on Zulip Mario Carneiro (May 26 2018 at 13:54):

this line

notation `⊥` := has_bot.bot _

should appear exactly once in mathlib, in bounded_lattice.lean

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:55):

I got bored trying to work out why it was broken

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:55):

I am under time pressure

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:55):

had

view this post on Zulip Mario Carneiro (May 26 2018 at 13:56):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (May 26 2018 at 13:59):

How about this for a readable proof?

example : (((1 : ) + 5) / 2) ^ 2 = ((1 : ) + 5 ) / 2 + 1 :=
have h : (0 : )  5 := by norm_num,
begin
  rw [pow_two, div_mul_div, mul_add, mul_one, add_mul, one_mul,  pow_two, sqr_sqrt h],
  ring,
end

view this post on Zulip 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 α,
  rw [mul_sub,mul_one,add_div,mul_add,add_mul,add_mul], -- meh
  simp [root_5_squared],
  norm_num, -- unknown exception while type-checking theorem
end

view this post on Zulip Kevin Buzzard (May 26 2018 at 13:59):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:00):

Why isn't this easy

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:00):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:00):

goal after simp is

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:01):

I must have taken a wrong turn

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:01):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:01):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:01):

you need ring for all that

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:02):

in R

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:02):

because if that's not easy

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:02):

then what kind of an R have you got here

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:02):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:03):

I completely understand the other approach

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:03):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:03):

I can always fall back on Nicholas' construction

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:03):

which indeed I will ultimately fall back on

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:04):

I get it

view this post on Zulip Mario Carneiro (May 26 2018 at 14:04):

1 sec

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:04):

Sorry to moan

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:04):

I am giving an important talk

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:05):

and I want it to be _really good_

view this post on Zulip Mario Carneiro (May 26 2018 at 14:05):

I believe it can be done with a short tactic invoke

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:05):

so I want to make a really professional job of it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:07):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:07):

one further step towards professional

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:07):

No more errors

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:08):

aargh that's a lie

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:09):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:09):

what time is it now?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:10):

I have loads of errors in mathlib

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:10):

I've tried everything

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:10):

I might reboot my computer

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:10):

and recompile all .olean files

view this post on Zulip Kenny Lau (May 26 2018 at 14:10):

are you trying to prove anything?

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:10):

but that's all I can think of

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:11):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:11):

I'll push

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:12):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:12):

But I want it to look sexy

view this post on Zulip Mario Carneiro (May 26 2018 at 14:13):

you could import data.real.basic instead

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:22):

what

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:27):

@Kevin Buzzard do you like direct proofs?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:28):

but that defeats the purpose of the presentation

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:28):

This is somehow awful

view this post on Zulip Mario Carneiro (May 26 2018 at 14:28):

it makes it look nice and readable

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:28):

but it's much better than nothing

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:28):

But I don't want it to be readable

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:28):

I want it to be trivial

view this post on Zulip Kenny Lau (May 26 2018 at 14:28):

what

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:28):

An obscure one-liner?

view this post on Zulip Mario Carneiro (May 26 2018 at 14:28):

you didn't like my ring solution?

view this post on Zulip Kenny Lau (May 26 2018 at 14:29):

I thought you're teaching rigour

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:29):

minus the by rw ... things

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:29):

I don't understand -- what ring solution?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:29):

:D

view this post on Zulip Kenny Lau (May 26 2018 at 14:30):

I can't delete my own messages...

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:30):

I want as many solutions as I can

view this post on Zulip Kevin Buzzard (May 26 2018 at 14:31):

And we vote for the most beautiful

view this post on Zulip Kenny Lau (May 26 2018 at 14:31):

beauty is in the eye of the beholder

view this post on Zulip Kenny Lau (May 26 2018 at 14:31):

in this case, you

view this post on Zulip Kenny Lau (May 26 2018 at 14:31):

it's you who is/are presenting

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:33):

I still don't know what @Kevin Buzzard wants

view this post on Zulip Kenny Lau (May 26 2018 at 14:33):

what is the goal of this?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:37):

I guess you could write the middle line as (1 - √5^2) / 4 for extra clean

view this post on Zulip Kenny Lau (May 26 2018 at 14:37):

low-tech one-liners:

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:38):

(is changing the definition allowed?)

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:40):

not very different from the one above...

view this post on Zulip Mario Carneiro (May 26 2018 at 14:41):

it's based on reid's

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 26 2018 at 14:43):

still avoiding ring as usual :P

view this post on Zulip Kenny Lau (May 26 2018 at 14:44):

I like my new definition

view this post on Zulip Kenny Lau (May 26 2018 at 14:44):

who likes my new definition

view this post on Zulip Mario Carneiro (May 26 2018 at 14:44):

I think your definition is nicer if you are going to define both alpha and beta

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 14:46):

that's what I did with the add_mul and mul_add

view this post on Zulip 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 :=
by simp [α, β, div_mul_div, add_mul, mul_add, sqrt_5_mul_self]; norm_num1

view this post on Zulip Kenny Lau (May 26 2018 at 14:46):

low-tech :P

view this post on Zulip Mario Carneiro (May 26 2018 at 14:46):

A long rw proof is hard to read though

view this post on Zulip Mario Carneiro (May 26 2018 at 14:47):

unless you step through it

view this post on Zulip Kenny Lau (May 26 2018 at 14:47):

I thought @Kevin Buzzard wants a one-liner

view this post on Zulip Mario Carneiro (May 26 2018 at 14:47):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 14:47):

I think we have that already

view this post on Zulip Mario Carneiro (May 26 2018 at 14:48):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:01):

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

view this post on Zulip Kenny Lau (May 26 2018 at 15:02):

then why wouldn't you write down every step

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:02):

All of this stuff is great

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:02):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:02):

You have never thought about steps

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:03):

You just answer the question

view this post on Zulip Mario Carneiro (May 26 2018 at 15:03):

I presume that will be part of the talk

view this post on Zulip Mario Carneiro (May 26 2018 at 15:03):

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

view this post on Zulip Mario Carneiro (May 26 2018 at 15:03):

and you have to use those rules to prove things

view this post on Zulip Mario Carneiro (May 26 2018 at 15:03):

the sense of "step" is not far from this

view this post on Zulip Kevin Buzzard (May 26 2018 at 15:09):

Yes exactly

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (May 26 2018 at 16:37):

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

view this post on Zulip Kenny Lau (May 26 2018 at 16:37):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 26 2018 at 16:38):

move it to point3.lean

view this post on Zulip Nicholas Scheel (May 26 2018 at 16:40):

done!

view this post on Zulip Nicholas Scheel (May 26 2018 at 16:43):

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

view this post on Zulip Kenny Lau (May 26 2018 at 16:44):

where are you stuck in?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2018 at 17:08):

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

view this post on Zulip Johan Commelin (May 26 2018 at 17:09):

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

view this post on Zulip Kenny Lau (May 26 2018 at 17:09):

proving that it is injective needs work also

view this post on Zulip Johan Commelin (May 26 2018 at 17:10):

That is the linear independence of 1 and alpha

view this post on Zulip Nicholas Scheel (May 26 2018 at 17:15):

sure, why not ;D

view this post on Zulip Kenny Lau (May 26 2018 at 17:15):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:09):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:10):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:10):

\surdfor square roots in maths mode, not \sqrt

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:10):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:10):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:15):

I did some Fibonacci stuff

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:15):

and some logic stuff

view this post on Zulip Kevin Buzzard (May 26 2018 at 21:15):

and we looked at why induction was a theorem in Lean

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (May 26 2018 at 21:36):

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

view this post on Zulip Kenny Lau (May 26 2018 at 22:41):

hmm, I wonder if we can shorten it

view this post on Zulip Kenny Lau (May 26 2018 at 22:58):

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

view this post on Zulip Nicholas Scheel (May 26 2018 at 22:58):

go for it!

view this post on Zulip Nicholas Scheel (May 26 2018 at 22:58):

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

view this post on Zulip Nicholas Scheel (May 26 2018 at 22:59):

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

view this post on Zulip Kevin Buzzard (May 26 2018 at 23:03):

It proves identities between explicit real numbers

view this post on Zulip Kevin Buzzard (May 26 2018 at 23:03):

And inequalities etc

view this post on Zulip Nicholas Scheel (May 26 2018 at 23:05):

cool :simple_smile:

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 26 2018 at 23:16):

I golfed off a lot of lines from here

view this post on Zulip Nicholas Scheel (May 26 2018 at 23:18):

that’s great :smiley:

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (May 26 2018 at 23:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (May 26 2018 at 23:29):

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

view this post on Zulip Kenny Lau (May 26 2018 at 23:30):

well there's not a huge difference

view this post on Zulip Reid Barton (May 26 2018 at 23:38):

I haven't used show in tactic mode!

view this post on Zulip Nicholas Scheel (May 26 2018 at 23:39):

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

view this post on Zulip Kenny Lau (May 27 2018 at 01:27):

@Nicholas Scheel I hope you don't mind

view this post on Zulip Kenny Lau (May 27 2018 at 01:28):

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

view this post on Zulip Kenny Lau (May 27 2018 at 01:33):

TODO: incorporate this

view this post on Zulip Nicholas Scheel (May 27 2018 at 01:42):

not at all, that’s cool! thanks!

view this post on Zulip Kenny Lau (May 27 2018 at 02:00):

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

view this post on Zulip Kenny Lau (May 27 2018 at 02:00):

done

view this post on Zulip Chris Hughes (May 27 2018 at 11:56):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:01):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:02):

And I've started separating the two

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:10):

However

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:11):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:11):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:11):

and this can be used to guide development of mathlib

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:13):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:13):

In the 144 proof we don't need full QR

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:13):

but we need Gauss' Lemma and Euler's Criterion

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:14):

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

view this post on Zulip Kenny Lau (May 27 2018 at 12:29):

instance : decidable_linear_ordered_comm_ring α :=

view this post on Zulip Kenny Lau (May 27 2018 at 12:29):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:43):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:43):

(why doesn't sqrt work in LaTeX?)

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:43):

He proved it was an ID?

view this post on Zulip Kenny Lau (May 27 2018 at 12:45):

He proved it was an ID?

yes

view this post on Zulip Kenny Lau (May 27 2018 at 12:45):

(althought I didn't use that)

view this post on Zulip Kenny Lau (May 27 2018 at 12:45):

(I used norm to prove that Zalpha is ID)

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

yes

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

which is tantamount to proving that sqrt5 is irrational

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:46):

and so you need to prove irrationality#

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:46):

right

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

on hindsight I should have used the embedding

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

but I still want to have the norm

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:46):

I was suggesting that Mario might have done that already

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

the norm is useful

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:46):

Sure

view this post on Zulip Kenny Lau (May 27 2018 at 12:46):

sure

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:46):

And your norm commutes with Mario's

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:47):

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

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:47):

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

view this post on Zulip Kenny Lau (May 27 2018 at 12:47):

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

view this post on Zulip Kenny Lau (May 27 2018 at 12:47):

because alpha is not an element of Z[sqrt5]

view this post on Zulip Kenny Lau (May 27 2018 at 12:47):

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

I know

view this post on Zulip Kenny Lau (May 27 2018 at 12:48):

I'll do it when I finish lunch

view this post on Zulip Kevin Buzzard (May 27 2018 at 12:48):

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

view this post on Zulip 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

view this post on Zulip Nicholas Scheel (May 27 2018 at 12:55):

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

view this post on Zulip Kenny Lau (May 27 2018 at 15:35):

done

view this post on Zulip Kenny Lau (May 27 2018 at 15:35):

now the long proof that 5 is irrational is gone

view this post on Zulip 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)

view this post on Zulip Kenny Lau (May 27 2018 at 15:50):

completely pointless theorem

view this post on Zulip Kenny Lau (May 27 2018 at 15:50):

Gal(Zalpha/Z) = C2

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 27 2018 at 15:51):

sure

view this post on Zulip Kenny Lau (May 27 2018 at 16:24):

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

view this post on Zulip Kenny Lau (May 27 2018 at 16:24):

lol I did it

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:37):

nice!

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:37):

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

view this post on Zulip 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α

view this post on Zulip Kenny Lau (May 27 2018 at 17:12):

look at what I did

view this post on Zulip 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

view this post on Zulip 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).
Proof: link.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2018 at 19:36):

how are those defined?

view this post on Zulip Mario Carneiro (May 27 2018 at 19:41):

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

view this post on Zulip Mario Carneiro (May 27 2018 at 19:43):

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

view this post on Zulip Kenny Lau (May 27 2018 at 20:44):

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

view this post on Zulip Kenny Lau (May 27 2018 at 20:44):

what am i doing

view this post on Zulip Kenny Lau (May 27 2018 at 20:45):

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

view this post on Zulip Kenny Lau (May 27 2018 at 20:45):

Wikipedia calls its little brother psi

view this post on Zulip Mario Carneiro (May 27 2018 at 21:36):

that one is true for the continuous extension too

view this post on Zulip Mario Carneiro (May 27 2018 at 21:36):

I call the little brother phi bar

view this post on Zulip Mario Carneiro (May 27 2018 at 21:36):

because it's the conjugate of phi

view this post on Zulip Nicholas Scheel (May 27 2018 at 22:24):

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

view this post on Zulip Kenny Lau (May 27 2018 at 22:27):

@Kevin Buzzard what do you think?

view this post on Zulip Kenny Lau (May 28 2018 at 00:28):

patchily converted everything to Zalpha

view this post on Zulip Kevin Buzzard (May 28 2018 at 03:12):

I don't care about names

view this post on Zulip Kevin Buzzard (May 28 2018 at 03:12):

I call things lemma 3.1

view this post on Zulip Kevin Buzzard (May 28 2018 at 03:13):

What do I know about names


Last updated: May 14 2021 at 19:21 UTC