Zulip Chat Archive

I mentioned on the chat earlier today that I was going to have a day off work, but I didn't say why. I am 50 today (I have been for ten minutes in fact), which some people think is a big deal. I've spent so much time over the last few months just doing basic number theory / topology with random undergraduates many of whom do not even speak on this forum, I've had a really good time, it's meant that I've got behind on so many things but honestly Lean has changed my life for the better and I'm so pleased to be involved. Oh wow so much stuff I didn't know about!

Kevin Buzzard (Sep 20 2018 at 23:19):

There are char polys?

Kevin Buzzard (Sep 20 2018 at 23:19):

This is just ridiculous, there is stuff here. It should all go in the "what's new in Lean maths" thread.

Kevin Buzzard (Sep 20 2018 at 23:20):

oh what a complete surprise!

Kevin Buzzard (Sep 20 2018 at 23:21):

I think Johan is pretty competent at modular forms :-)

Kevin Buzzard (Sep 20 2018 at 23:29):

I am stunned.

Kevin Buzzard (Sep 20 2018 at 23:30):

Nobody ever gives me anything for my birthday, it is not taken at all seriously around here. I just get a new pair of trousers from my partner and that's it :-)

Kevin Buzzard (Sep 20 2018 at 23:30):

This year I got modular forms!

Mario Carneiro (Sep 20 2018 at 23:32):

My birthday present is a bit late, but I should have that refactor out today

Kevin Buzzard (Sep 20 2018 at 23:33):

rofl

Kevin Buzzard (Sep 20 2018 at 23:35):

I would never dream of hurrying you. Sometimes people have to wait. Patrick really wants perfectoids done but I was talking to Chris over lunch and confessing that I was skipping lemmas about valuations because even though they "should be there", I wasn't going to put them there until we needed them. Chris said that this wasn't really the way to write Lean code. But if I write it properly Patrick will have to wait even longer. That's why ultimately I decided to start at the top to find out how many sorrys there are. Maybe I can even estimate how much work is left, in some sense. But as you once said, it's an open source project, people work on it when they can.

Mario Carneiro (Sep 20 2018 at 23:36):

Oh it's no hurry, it's timing :)

Kevin Buzzard (Sep 20 2018 at 23:42):

There are differentiable functions!

Kevin Buzzard (Sep 20 2018 at 23:42):

About time!

Johan Commelin (Sep 21 2018 at 04:51):

Happy birthday Kevin! :birthday: :smiley:

Sean Leather (Sep 21 2018 at 05:39):

Happy birthday! :tada:

Patrick Massot (Sep 21 2018 at 06:44):

Happy birthday! :birthday: :fireworks: :confetti:

Mario Carneiro (Sep 21 2018 at 06:45):

people keep finding more exciting emoji

Kenny Lau (Sep 21 2018 at 06:46):

:birthday: :birthday: :birthday: :birthday: :birthday: :birthday: :birthday: :birthday: :birthday: :birthday:

Sean Leather (Sep 21 2018 at 06:46):

:five: :zero: :double_exclamation:

Kenny Lau (Sep 21 2018 at 06:46):

520469842636666622693081088000000

Mario Carneiro (Sep 21 2018 at 06:48):

not to be confused with 10^(10^66.28958573684642)

Kevin Buzzard (Sep 21 2018 at 11:57):

Thank you Johan for the post on the "what's new" stream and thank you all of you for the repo. I am overwhelmed. You inspired me to write this: https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean

Kevin Buzzard (Sep 21 2018 at 11:58):

It's a place for wishes.

Reid Barton (Sep 21 2018 at 12:11):

I heard maybe we should try to formalize the Riemann zeta function

Johan Commelin (Sep 21 2018 at 12:11):

@Kevin Buzzard Thanks for writing that question on mathoverflow. I am really excited and I look forward to the reactions.

Johan Commelin (Sep 21 2018 at 12:11):

I heard maybe we should try to formalize the Riemann zeta function

How much of that is already done in formal abstracts?

Kevin Buzzard (Sep 21 2018 at 12:14):

That's a really good suggestion. I think Hales' definition had sorries. Oh -- the issue is the analytic continuation. Convergence shouldn't be hard for the experts now we have exp :-)

Patrick Massot (Sep 21 2018 at 12:14):

https://github.com/thalesant/formalabstracts/blob/riemann_hypothesis/folklore/complex.lean#L246

Kevin Buzzard (Sep 21 2018 at 12:15):

$n^s := \exp(s\log n)$ oh crap we need log too

Patrick Massot (Sep 21 2018 at 12:15):

But convergence is also not proved

Kevin Buzzard (Sep 21 2018 at 12:16):

Wait do we have complex.pow?

Kevin Buzzard (Sep 21 2018 at 12:16):

Does his definition compile?

Patrick Massot (Sep 21 2018 at 12:16):

https://github.com/thalesant/formalabstracts/blob/riemann_hypothesis/folklore/complex.lean#L153

Kevin Buzzard (Sep 21 2018 at 12:17):

nice to see pi there -- I heard we had that.

Kevin Buzzard (Sep 21 2018 at 12:17):

But this is just real log we need; complex exp but real log.

Kevin Buzzard (Sep 21 2018 at 12:17):

So we need that exp is strictly increasing and continuous, and enough analysis to show that it yields a bijection between the reals and the positive reals.

Reid Barton (Sep 21 2018 at 12:41):

Yeah, this is an example of how it's tricky to say exactly what it means to define something. What Hales has done here is define a function ζ which, "externally", we can prove is equal to the usual zeta function.
Actually he only did this assuming a couple axioms, but the axioms are easy to avoid--just define ζ in terms of the axioms if they are true, and define it to be 37 if they are false.
This sort of thing already happened implicitly where he defined exp as a tsum and real.log as a sup--there are side conditions that you need here to make sure that you defined what you expected to define.

Kevin Buzzard (Sep 21 2018 at 12:55):

So the first goal is to give a sorry-free definition of an explicit function from C -> C which away from s = 1 agrees with the Riemann zeta function, possibly after invoking known mathematical theorems. Can we make it computable?

Kevin Buzzard (Sep 21 2018 at 12:55):

Can someone put Riemann Zeta Function on the MO thread?

Kevin Buzzard (Sep 21 2018 at 12:56):

I don't want to spam my own MO post with my own answers, this isn't an exercise in self-advertisement, it's a research proposal.

Kevin Buzzard (Sep 21 2018 at 12:56):

Collaborators wanted.

Johan Commelin (Sep 21 2018 at 15:30):

Right, I don't think you should spam it. But we shouldn't spam it either... I'dd be very interested in what "tabula rasa" mathematicians come up with. I might post something tomorrow.

Mario Carneiro (Sep 21 2018 at 16:27):

Chris had only just finished pi in time for the birthday surprise, but real log is almost there and complex log can be done with a bit more work. See https://leanprover.zulipchat.com/#narrow/stream/141825-kbb/subject/sine.20and.20cosine.20and.20pi/near/134258931

Bryan Gin-ge Chen (Sep 21 2018 at 16:28):

Could that stream be made public now that the birthday surprise has been revealed?

Johannes Hölzl (Sep 21 2018 at 16:33):

look for kbb, it should be public (at least I don't see a lock anymore)

Johan Commelin (Sep 21 2018 at 17:00):

@Kevin Buzzard Wow, I think the response to your mathoverflow post is really positive! I expected a lot (a lot!) more skepticism from the community. Maybe mathoverflow isn't completely representative. But still, I really like this. Apart from the thing about Inter-Universal Teichmuller Theory all the other proposals are actually nice (somewhat ambitious) and realisable.

Johan Commelin (Sep 21 2018 at 17:02):

The post has an immense rate of upvotes (a lot faster then your post about perfectoids in Lean). And the post doesn't even mention that you are turning 50 today :grinning:

Kevin Buzzard (Sep 21 2018 at 17:08):

Johan I would like to personally thank you for your idea about pi, and also Patrick for your suggestion about the T_2 project. I am still really flattered and stunned, and really touched. I think everyone should try to formalise one of their theorems. I don't understand formal abstracts. Are they waiting for Lean 4 or what? I don't have any unrealistic ambitions. I'm not thinking that in 1 year we will have Lean 4 with the global Langlands conjectures. But all this internet noise I'm trying to make today is because I want to train mathematicians right now, so we are ready to deal with what what might be the huge task of porting Mathlib to Lean 4. Johannes is leaving academia and Mario cannot do it alone. We need more volunteers and they need training. We have now seen that it takes one year to turn an incoming first year undergraduate into Chris Hughes or Kenny Lau. Let's make a few more of them with Lean 3.4.2 and worry about Lean 4 later. Let's see what we can do with a first year PhD student. There are plenty of other things to worry about before Lean 4. For example categories and canonical isomorphisms / transport de structure. Lean 4 is not magically going to solve those, or at least I don't think it is.

Johan Commelin (Sep 21 2018 at 17:10):

My pleasure! It was a lot of fun to work on these projects behind your back. But really @Chris Hughes deserves an insane amount of credit. He did all the hard work on exp and pi all by himself.

Kevin Buzzard (Sep 21 2018 at 23:41):

well that was eventful. Thank you all for the encouragement. If anyone wants to write a guest blog post just ask.

Kenny Lau (Sep 22 2018 at 03:53):

@Mario Carneiro @Patrick Massot What do you two think about the ideas here?

Mario Carneiro (Sep 27 2018 at 02:14):

Woo, Kevin's MO question just hit the HNQ list, which means it will be seen across all of stack overflow

Johan Commelin (Sep 27 2018 at 03:06):

Let's see what happens...

Reid Barton (Sep 27 2018 at 04:30):

Kevin's question generated a noticeable bump in users on the stats page

Kevin Buzzard (Sep 27 2018 at 06:33):

"Locally presentable categories and combinatorial model categories please. Is it feasible ? I am actually discovering this thread and know nothing about Lean." says someone on the MO question, @Scott Morrison ?

Johan Commelin (Sep 27 2018 at 06:54):

I think @Reid Barton was talking about similar stuff in Orsay. This shouldn't be too far.

Reid Barton (Sep 27 2018 at 11:21):

Yesterday I wrote about half of a detailed outline for model categories.
Actually I wrote all of the parts up through constructing combinatorial model categories if you don't want any examples :smile:

Johan Commelin (Sep 21 2019 at 03:48):

Happy birthday, @Kevin Buzzard :cake:

Kevin Buzzard (Sep 21 2019 at 12:58):

rofl so I was expecting Galois cohomology and Tate-Shafarevich groups :-)

Johan Commelin (Sep 21 2019 at 13:36):

Yeah, we were almost done with

instance : fintype (Sha E) :=

but gave up when we realised your birthday was today, and not tomorrow...

Johan Commelin (Sep 21 2021 at 03:47):

Happy birthday, @Kevin Buzzard :birthday:

Kevin Buzzard (Sep 21 2021 at 05:56):

Thank you! My birthday is traditionally a good Lean day, for example in 2019 it was the day that things like $\pi$ and sine/cosine were formalised. This year is going to be no exception, but for more details we have to wait until the official announcement...(which might actually be tomorrow, at least in the UK, and because of Covid restrictions I'm even missing the canapés, but I can live with this). The community goes from strength to strength...

Johan Commelin (Sep 21 2022 at 04:01):

Happy birthday to you! Dear @Kevin Buzzard :birthday:

Kevin Buzzard (Sep 21 2022 at 04:06):

Happy CPP deadline day too, to everyone who's celebrating that! Looking forward to reading the sphere eversion paper!

Last updated: Dec 20 2023 at 11:08 UTC