Zulip Chat Archive

Stream: kbb

Topic: hello


view this post on Zulip Welcome Bot (Sep 11 2018 at 20:26):

Welcome to #kbb.

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:28):

This is a test: can anyone hear me?

view this post on Zulip Reid Barton (Sep 11 2018 at 20:28):

Yes

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:28):

Does anyone has another Zulip account and could check what is visible?

view this post on Zulip Reid Barton (Sep 11 2018 at 20:28):

I thought about this, but I'm not sure whether the stream would be visible to external people. Yeah

view this post on Zulip Reid Barton (Sep 11 2018 at 20:29):

Or, just remove me temporarily.

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:29):

Funnily, I don't seem to be allowed to do that

view this post on Zulip Simon Hudon (Sep 11 2018 at 20:31):

I see you

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:32):

I'm creating another account

view this post on Zulip Simon Hudon (Sep 11 2018 at 20:32):

Also: this is a great idea

view this post on Zulip Simon Hudon (Sep 11 2018 at 20:33):

Did you need the help of an administrator to create this stream?

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:33):

No

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:34):

I think this stream is safe

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:34):

The point is that group PM is not suitable for what we were doing. That generates too many notifications

view this post on Zulip Simon Hudon (Sep 11 2018 at 20:35):

Amen

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:36):

Reid, do you see things here?

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:37):

Reid should be back in

view this post on Zulip Reid Barton (Sep 11 2018 at 20:38):

Yep, I am now.

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:38):

And should see the full history, which is another advantage compared to group PM

view this post on Zulip Reid Barton (Sep 11 2018 at 20:38):

Indeed I can

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:38):

(this was an option when creating the stream)

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:39):

Ok, let's stop using the group PM and its endless series of emails and notification popups

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:39):

Did you need the help of an administrator to create this stream?

No

view this post on Zulip Patrick Massot (Sep 11 2018 at 20:41):

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

view this post on Zulip Johan Commelin (Sep 12 2018 at 02:22):

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

Shouldn't this go into a new thread :rolling_on_the_floor_laughing:

view this post on Zulip Johan Commelin (Sep 12 2018 at 02:24):

To answer your question: fast_matrix is now obsolete, since @Jack Crawford pushed an implementation that is a lot more fleshed out. His implementation is both supposed to be faster to compute with and easier to type. You can use the equation compiler to grab the a b c d out of a 2x2 matrix, which makes for readable definitions.

view this post on Zulip Johan Commelin (Sep 12 2018 at 02:25):

Also: very good idea to create a private stream. I didn't know this was possible. We should have done that 1 week ago.

view this post on Zulip Johan Commelin (Sep 12 2018 at 02:26):

The cool side effect is that we can give Kevin access, and he can read through the history of all of our discussions :lol:

view this post on Zulip Kenny Lau (Sep 16 2018 at 08:48):

ok so we have 4 days left

view this post on Zulip Kenny Lau (Sep 16 2018 at 08:48):

can we come up with a realistic list of goals

view this post on Zulip Kenny Lau (Sep 16 2018 at 08:48):

or a list of realistic goals?

view this post on Zulip Patrick Massot (Sep 16 2018 at 16:08):

Mario, do you see anything in this repo that could hope to get into mathlib?

view this post on Zulip Johan Commelin (Sep 17 2018 at 04:03):

Like I said, I'll be gone on Wednesday, so I can only contribute today and tomorrow.

view this post on Zulip Johan Commelin (Sep 17 2018 at 04:04):

I think either: we start cleaning up; or we focus on the Hecke operator (on the complex vector space (=module :lol:) of modular forms.

view this post on Zulip Johan Commelin (Sep 17 2018 at 04:04):

This second option will probably force us to clean up other stuff as well.

view this post on Zulip Johan Commelin (Sep 17 2018 at 04:05):

Otoh, we could also leave the modular form part of the repo as it is.

view this post on Zulip Johan Commelin (Sep 17 2018 at 04:05):

And then we could focus all our time on exp and friends.

view this post on Zulip Johan Commelin (Sep 18 2018 at 06:41):

:bell: We have 99 commits in the kbb repository! Well done to everyone who contributed!

view this post on Zulip Patrick Massot (Sep 18 2018 at 08:52):

What's the status of the Hecke operator file? I don't even understand the maths here. What is the meaning of the first displayed formula at https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula? Is each term in the sum meant to be well defined? Or only the sum? If I naively try to change (a b c d) by multiplication by a element of SL2Z and use the weight formula for f, I don't seem to get the same term.

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:04):

You should get the same term, right? Or did I mess something up. I was quite convinced that every term in the sum was well-defined.

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:05):

But maybe we should just delete this file... I think I aimed to high.

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:06):

I don't understand the wikipedia page, so you don't need to mess up anything

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:06):

What is the pen and paper proof that each term in the sum is well-defined?

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:07):

I must be missing something obvious

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:08):

(cz+d)kf(az+bcz+d)=(cz+d)kf((abcd)z)(cz + d)^{-k} f(\frac{az + b}{cz + d}) = (cz + d)^{-k} f(\begin{pmatrix} a & b \\ c & d \end{pmatrix}z), is that right?

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:08):

yes

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:08):

So now we take another representative: M(abcd)M\begin{pmatrix}a & b \\ c & d \end{pmatrix}

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:09):

The trouble is that a,b,c,d(cz+d)a, b, c, d \mapsto (cz+d) is not a group morphism

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:10):

Hmm, I'm also getting myself confused.

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:11):

If that were a group morphism then everything would be obviously ok

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:12):

Too bad we can't ask Kevin

view this post on Zulip Reid Barton (Sep 18 2018 at 09:13):

It shouldn't be a group morphism, it should be a 1-cocycle, or something. Right? Because zz is changing too

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:14):

oh yes, z is changing

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:14):

I think it's not changing enough on my paper

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:18):

Ok, it works now

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:19):

You can continue to do number theory, it's alright

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:19):

It was only a stupid copy-paste mistake

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:20):

It also works on my paper

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:20):

So, we've proven it! Let's move on to the next maths theorem (-;

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:20):

It shouldn't be that hard to Lean (modulo those f***ing cast and coes)

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:21):

Right, Kenny did a lot of useful stuff (-;

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:21):

But all those actions of matrices on each other, and on the upper half plane...

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:21):

That's going to be quite a pain.

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:25):

@Patrick Massot Are you willing to take a shot at it?

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:25):

I may try in the afternoon

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:53):

I cleaned up a tiny bit but several things are weird. First I cannot sorry the proof. Lean complains there are remaining meta-variables, but I don't see where. And I have an hypothesis H: A ≈ B that I found no way to destruct into the existence of P in SL2 such that B = PA. This is not such a suprise because the beginning of the proof is really a mess

view this post on Zulip Patrick Massot (Sep 18 2018 at 09:54):

I think this is a very bad start. @Johannes Hölzl could you have a look?

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:56):

Right... my brain stopped working after I wrote the start of that file. Guess why...

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 10:04):

@Patrick Massot where should I look? I have no idea what a Hecke operator is. Did you push your commits, I don't see anything in kbb.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:05):

There is a file called Hecke_operator or something

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:05):

The mathy definition is here: https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:06):

To prove that the sum is over a finite set, we need to use the stuff that you cleaned up.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 10:07):

Hm, the statements shouldn't change, besides reduce_def which is now reduce_eq1, reduce_eq2, reduce_eq3`.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:12):

Right, line 12 should be

  haveI := SL2Z_M.finiteness m (ne_of_gt h),

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:13):

Crap. I forgot to push

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:14):

And I left my computer

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:39):

Fixed

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:40):

@Johannes Hölzl Now you can have a look, sorry about the false start

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:52):

I'm a bit scared about the fact that we only know that SL2Z_H is a group action.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:52):

It seems like we would want to know that MAT2_H is a monoid action.

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:53):

Oh yes, we need that

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:53):

But refactoring SL2Z into a subtype of MAT2 give me a headache

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:53):

I thought this was the reason you put det > 0 everywhere instead of det = 1

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:53):

Because that means we have to go through all of Kenny's code again

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:54):

And this is why I don't understand how term mode code could be easier to maintain

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:54):

They set things up in the correct way the first time.

view this post on Zulip Patrick Massot (Sep 18 2018 at 10:54):

No, that's not what refactoring means

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:54):

Instead of me: I only get it right after 42 attemts.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:54):

You're right.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:55):

But I agree that it is really confusing that we can not unfold that equivalence between A and B

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:55):

After we have that, we could try to just battle on.

view this post on Zulip Johan Commelin (Sep 18 2018 at 10:55):

Although it might be nicer to have the monoid action do some work for us

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:25):

Oh my goodness. If we want to generalise stuff to monoid actions there I'm so scared that everything breaks. I've learned a lesson: first try to think out some good API's.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:28):

@Johannes Hölzl So we have two problems: (1) how do we unfold the equivalence in hecke_operator.lean.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:29):

By definition A and B are equivalent if there is an M : SL2Z such that A = MB.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:29):

We want to get that M out.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:30):

And (2), to get a readable (and workable) version of the Hecke operator, it would be good to have A • z where A is any 2x2-matrix with integer coefficients, and z : ℍ.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:31):

In the end we will get (M • B) • z, and then we want to know that this is the same thing as M • (B • z)

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:31):

So, first I fixed the basic definition. We currently had some missing goals (the anonymous constructor was outside tactic mode, so some type class instances where missing)

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:35):

Ok, I guess that helps a bit (-;

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:36):

I suspected something like this

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:37):

@Johannes Hölzl Do you think it would be better if Möbius_transform turned into • notation?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:38):

Uh, overloading could be problematic, at least annoying...

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:38):

Why do we know that A an B are representatives?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:38):

so inreps?

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:39):

No, we don't know that

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:39):

We don't need that

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:39):

They are merely "any representative"

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:39):

This reps story is all used up in the finiteness fact

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:39):

We won't use it again

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:39):

in this proof

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:40):

We won't use it again

We promise.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:40):

but we could use them to define the Hecke operator? Then we don't need to lift the quotients...

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:40):

of course, later we need the proof anyway

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:40):

Hmm, I suppose so.

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:41):

That would be cheating

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:41):

And "later" will be after the birthday party.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:43):

@Johannes Hölzl Why would we be overloading ? The monoid action MAT2 → ℍ → ℍ can be an instance of has_scalar right?

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:43):

We don't have MAT2, but I think every monoid action should be an instance of has_scalar.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:43):

ah, okay. I thought you wanted to add another notation...

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:43):

It's interesting to know how far one should be allowed to go into definition cheating. Say I want to prove RH in Lean. I define the usual zeta, call it zeta', and then define zeta(z) to be zeta'(z) if z is not a surprising zero of zeta', and one otherwise. Then I prove RH, and all is left is proving my definition of zeta is equivalent to the usual one...

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:45):

what do you mean you want t get the M out? Like rintros A B ⟨M, eq⟩, works...

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:45):

I guess so

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:45):

I think it works because of your previous fix

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:46):

It definitely didn't work this morning

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:46):

Good!

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:46):

Because now we can rw along eq, and then the fight begins!

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:47):

The current state is

...
A B : Mat m,
M : SL2Z,
eq : SL2Z_M m M A = B,
weight_f :
   (M : SL2Z) (z : {x // x  }),
    f «Möbius_transform» (M.a) (M.b) (M.c) (M.d) z, _⟩ =
      ((M.c) * z + (M.d)) ^ (k + 1) * f z
 1 / ((A.c) * z + (A.d)) ^ (k + 1) *
      f «Möbius_transform» (A.a) (A.b) (A.c) (A.d) z, _⟩ =
    1 / ((B.c) * z + (B.d)) ^ (k + 1) *
      f «Möbius_transform» (B.a) (B.b) (B.c) (B.d) z, _⟩

Is this what you want?

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:47):

Yep

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:47):

ah, okay. Its in kbb now

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:50):

by the way: it is surely good style to define Möbius_transform on Mat m instead fof integer tuples.

view this post on Zulip Patrick Massot (Sep 18 2018 at 11:50):

I hate this integer tuples thing. I don't understand why we don't use matrices everywhere

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:50):

Right, so why don't we define it on matrix (fin 2) (fin 2) R where R is a subring of ?

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:51):

Also, can we have a coercion from to fintype, that sends n to fin n?

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:51):

Then stuff becomes even more readable (-;

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:52):

@Patrick Massot I think we should. But with an old version of matrices it was hard to actually write down examples.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:53):

Hm, having a coerion from to Type would be nice!

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 11:54):

Ah, I see there is SL2Z_H. So maybe we want a similar form for Mat m?

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:54):

It is in the repo, but I haven't pushed yet.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:54):

Well, MAT2 really. And afterwards we can restrict to subtypes.

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:54):

Mat m is a bad algebraic structure

view this post on Zulip Johan Commelin (Sep 18 2018 at 11:55):

It isn't a monoid

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:09):

So, we have

@[simp] theorem one_val_ne {i j} (h : i  j) : (1 : matrix n n α) i j = 0 :=
by simp [one_val, h]

in the matrices file. I would like Lean to try and figure out on its own if h is satisfied. In fin 2 it should know that 0 ≠ 1.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:09):

Is this something that an auto_param like dec_trivial could do?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:09):

Okay, I added M_trans anyway.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:10):

How do I need to change the statement?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:11):

Either add a tactic: dec_tac := ``[exact dec_trivial] and use this: (h : i ≠ j . dec_tac)

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:11):

or use default parameter (h : i ≠ j := dec_trivial)

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:12):

I don't know if the default parameter work. If dec_trivial gets evaluated too early it might not work

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:12):

I'll try.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:13):

Ok, the M_trans is nice. So now we need to plug that into the definition of the Hecke operator.

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:15):

It isn't happy about meta def dec_tac : tactic unit := ``[exact dec_trivial]

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:16):

meta def dec_tac : tactic unit := `[exact dec_trivial]

maybe?

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:17):

That worked

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:19):

So now my goal is:

z : 
 (z + 0) / (1 + 0 * z) = z

If Kevin saw that goal...

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:19):

simp didn't kill it.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:19):

Does unfold_coes help?

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:21):

Is that a tactic?

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 12:21):

yes

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:24):

It doesn't help enough...

view this post on Zulip Johan Commelin (Sep 18 2018 at 12:25):

I'll go back to the Hecke operator for a moment.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:59):

Ok guys... I'm gone for a week. I might be able to check Zulip now and then, but I won't be able to do any serious Leaning until next week on Thursday.

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:59):

I'm looking forward to Kevin's reaction on Friday

view this post on Zulip Johan Commelin (Sep 18 2018 at 14:59):

Thanks for all your help so far! I really enjoyed it!

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:59):

Thanks for all your efforts

view this post on Zulip Patrick Massot (Sep 18 2018 at 14:59):

But we still haven't decided what will happen on Friday

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:21):

Seriously, what are we doing tomorrow? @Chris Hughes will you see Kevin tomorrow?

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:28):

Tomorrow is Thursday. I guess any cleaning up that we want to do should be done today or tomorrow. On Friday we give Kevin access to kbb and we PR the determinants file and the remainder of matrices.lean

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:29):

I don't think there is much in the modular form files that is ready to merge.

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:30):

What about sin and cos? We don't have pi yet, but we do have sin and cos.

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:30):

I would veto the current definition of sin

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:30):

unless it changed recently

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:30):

How come?

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:30):

What was wrong with it?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:31):

Would you write this on a blackboard?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:31):

def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:31):

come on

view this post on Zulip Kenny Lau (Sep 19 2018 at 09:31):

I don't see what's wrong with it

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:32):

Is it the definition in the UK?

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:32):

I think a PR on exp would be nice. Possibly including cos und sin. Hopefully that will induce a rampage by some Lean-fu experts to prove continuity.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:32):

I don't even know what definition of sin I saw. My training in analysis was terrible.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:33):

Possibly it was the analytic continuation of real.sin

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:33):

I don't know how real.sin was defined. Probably using angles etc...

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:33):

I'm going to have a serious bash on continuity today. The definition I saw was ((exp (z * I) - exp (-z * I))) / (2 * I)

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:33):

In France, sin z = (exp (z * I) - exp (-z * I)) * I) / (2*I)

view this post on Zulip Kenny Lau (Sep 19 2018 at 09:34):

is there any difference?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:34):

Yes. One is the definition people expect to see, the other one could be a useful lemma if Chris needs it

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:34):

I multiplied by i-i, Patrick divided by ii.

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:35):

Chris, why did you do that?

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:36):

It's easier to prove sin (x + y) because I have less division to deal with.

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:36):

Then you could use a lemma

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:36):

Actually I don't understand why you use these proofs for sin(x+y) etc.

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:37):

Which proofs should I use?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:37):

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:37):

That's the real life proof

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:38):

But I guess you should rather prove continuity and try to get pi

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:38):

And also answer my question: will you see Kevin tomorrow?

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:39):

Yes.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:42):

@Patrick Massot Why tomorrow? Don't you mean Friday? Or do you have some plan in mind?

view this post on Zulip Chris Hughes (Sep 19 2018 at 09:43):

I won't see him on Friday.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:44):

@Scott Morrison Could you give Kevin access when it is Friday 09:00 your time? Because then it is 00:00 his time, I think.

view this post on Zulip Scott Morrison (Sep 19 2018 at 09:44):

Sure.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:45):

Nice :lol:

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:54):

I meant Friday, sorry

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:55):

And @Kenny Lau isn't back in the UK at that point, I guess?

view this post on Zulip Kenny Lau (Sep 19 2018 at 09:55):

i'm not

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:55):

Patrick, were you thinking of physically giving him some gift? A print-out of the files :lol: ?

view this post on Zulip Patrick Massot (Sep 19 2018 at 09:57):

I wanted someone who could see his face and tell us.

view this post on Zulip Johan Commelin (Sep 19 2018 at 09:58):

Agreed, that would be nice.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 16:17):

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

That only proves the addition formulas for sin and cos when the arguments are real

view this post on Zulip Patrick Massot (Sep 19 2018 at 16:17):

oh yes

view this post on Zulip Mario Carneiro (Sep 19 2018 at 16:18):

I don't think there is any substitute for just doing the algebra in the complex case

view this post on Zulip Patrick Massot (Sep 19 2018 at 16:18):

I never thought about the complex case here

view this post on Zulip Patrick Massot (Sep 19 2018 at 16:18):

crazy

view this post on Zulip Reid Barton (Sep 19 2018 at 16:35):

no problem. then just show that two holomorphic functions which agree on the real line are equal :upside_down:

view this post on Zulip Patrick Massot (Sep 19 2018 at 16:53):

Great !

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:27):

This is so amazing! Awesome! That was an immense tour de force, Chris. Well done!

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:30):

I am about to go to bed. I'm sorry I won't be able to be online when Kevin gets his birthday present. I am sure that you guys will be able to break the surprise! I'll read up on it afterwards (-;

view this post on Zulip Scott Morrison (Sep 20 2018 at 22:36):

I think the plan is that in 24 minutes I will add Kevin to the kbb repository.

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:48):

@Scott Morrison Yes, that's a good plan!

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:48):

You can also add him to this stream on Zulip, and you can write a happy birthday post in the general stream.

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:49):

I should really go to bed now. Tomorrow I'll have 4 hard math-talks waiting for me...

view this post on Zulip Johan Commelin (Sep 20 2018 at 22:49):

Happy PR'ing (-;

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 23:10):

wtf?

view this post on Zulip Johan Commelin (Sep 21 2018 at 05:15):

@Kevin Buzzard We hope you will enjoy reading back through all our crazy conversations of the last 10 days. :stuck_out_tongue_wink:

view this post on Zulip Simon Hudon (Sep 21 2018 at 05:16):

Did we bash Kevin in any of it?

view this post on Zulip Patrick Massot (Sep 21 2018 at 06:49):

I don't remember doing it more than on the regular streams

view this post on Zulip Patrick Massot (Sep 21 2018 at 06:51):

Kevin: the conversation about this project started in group PM but then it was generating a huge mess of notification for everybody, and I eventually found out anybody could create private streams. So the story of this stream starts in the middle.

view this post on Zulip Patrick Massot (Sep 21 2018 at 06:55):

I think it's fair to point out that Johan came with this idea, on September 4th.

view this post on Zulip Patrick Massot (Sep 21 2018 at 06:57):

In order to understand the mess in the repository, it may be relevant to know that, beyond Johan's idea of a birthday pi, the unrealistic idea that I proposed was to formal abstract https://www.sciencedirect.com/science/article/pii/S0022314X96900396?via%3Dihub

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 11:07):

ROFL

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 11:09):

That is so funny. That is a fine abstract to formalise. It would be trivial if there was a half-decent API for modular forms, and Lean is perfect for that sort of thing.

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 11:11):

You could formalise a mathematically equivalent statement more easily -- the eigenvalues of a Hecke operator on a space of modular forms are the same as the eigenvalues of a corresponding Hecke operator on a certain group cohomology group, by a theorem of Eichler and Shimura. Formalising group cohomology would perhaps be easier than formalising modular forms -- I'm not really sure but it sounds easier to me. Group cohomology is just there waiting to be done.

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 11:13):

I wrote that paper after hearing a talk of Dinakar Ramakrishnan, when he mentioned that he had never seen a modular eigenform whose Hecke eigenvalues generated a non-solvable extension of the rationals. Talking to him afterwards it became clear that this was only because there were no computer programs to compute modular forms, and that we all knew exactly where to look. I took the trouble to look and there they were. Dinakar urged me to write it up.

view this post on Zulip Patrick Massot (Sep 21 2018 at 11:25):

We are not so far away from having Hecke operators (they almost act on functions of a fixed weight, and it shouldn't be so hard to show they act on holomorphic functions and preserve boundedness at infinity). We also have characteristic polynomial, and Johannes has been working towards Galois groups. But we mostly gave up when Johan pointed out that we would need that modular forms of a fixed weight form a finite dimensional subspace of holomorphic functions (we do have a vector space structure on holomorphic functions on the upper half plane).

view this post on Zulip Kevin Buzzard (Sep 22 2018 at 09:43):

aie, yes, finite-dimensionality is needed. A trivial consequence of the fact that the global sections of a line bundle on a compact Riemann surface are finite-dimensional, so by maths_undergraduate should do it. I'm going to try and build that tactic at Imperial.

Finite-dimensionality for the group cohomology would be a trivial consequence of the fact that a finite index subgroup of a finitely-generated group is finitely-generated, and the fact that SL(2,Z) is finitely-generated. I don't know how easy it is to prove the finite index result just by group theory, I am no algebraist. The proofs I know are topological. The group cohomology variant would be provably equal once we had something like Stokes' theorem.

view this post on Zulip Johan Commelin (Sep 22 2018 at 10:31):

We have the fact that S and T generate SL2Z in your birthday repo :lol:

view this post on Zulip Kevin Buzzard (Sep 22 2018 at 11:37):

Right. But for finite-dimensionality of the cohomology group for general levels we'll need that a finite index subgroup of a f.g. group is f.g. But I see what you're saying -- this is enough to prove that level 1 modular forms are finite-dimensional.

view this post on Zulip Kevin Buzzard (Sep 22 2018 at 11:37):

There is some kind of subtlety which I have only recently become aware of, and again it was a comment of @Reid Barton which clarified things for me. Without some general theory of global sections of line bundles on compact Riemann surfaces it's kind of a pain to prove that the space of modular forms is finite-dimensional. But it is finite-dimensional, so one can define the char poly of a Hecke operator to be "if the space is infinite-dimensional then 37, and if it's finite-dimensional then the char poly". This gives a sorry-free way of defining the char poly which is human-provably equivalent to the right thing. What one cannot do is to get away without defining the Hecke operator at all and just sorrying it -- because then the char poly has a sorry in too.

One of the things I realise I want now is for a bunch of mathematicians to come along and say "can you formalise theorem X or definition Y in Lean?" because questions such as that are ways of discovering what kind of an API a normal mathematician (perhaps with no Lean training) wants. Who cares about proofs, they are too hard. I know that Mario feels that a definition is pointless without an application. How about if the application is some statements of theorems or conjectures?


Last updated: May 18 2021 at 10:14 UTC