Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Logistics

Patrick Lutz (Jan 19 2021 at 17:57):

@Thomas Browning The recursion theory seminar (which both Jordan and I went to last semester) is apparently going to be at 1-2 pm on Fridays this semester. So maybe we should change the lean seminar meeting time

Thomas Browning (Jan 19 2021 at 18:01):

I'm free Thursdays and Fridays, anytime after 1pm.

Patrick Lutz (Jan 19 2021 at 18:01):

How about 2 pm on Fridays?

Patrick Lutz (Jan 19 2021 at 18:01):

@Jordan Brown Does 2 pm on Fridays work for you?

Patrick Lutz (Jan 19 2021 at 18:02):

@Chase Norman: see messages above. The seminar time may be changing to 2 pm on Fridays in case you want to join us some week

Jordan Brown (Jan 20 2021 at 04:36):

I can't do 2, since metamath is at 2, but I can do any time before 1 on Friday; before 1 on Thursdays also works for me

Jordan Brown (Jan 20 2021 at 04:36):

Also, I won't be around this Friday at all because I'm going to a funeral in the afternoon

Kevin Buzzard (Jan 20 2021 at 06:54):

What's Metamath?

Patrick Lutz (Jan 20 2021 at 07:02):

Kevin Buzzard said:

What's Metamath?

I think he means a grad course at Berkeley which is labelled "metamathematics" (rather than the proof assistant "metamath")

Patrick Lutz (Jan 20 2021 at 07:03):

Okay, I propose we meet at 2 pm on Friday for this week but discuss what time to pick for future weeks

Thomas Browning (Jan 22 2021 at 06:01):

@Jordan Brown I've golfed your insolvability proof.

Thomas Browning (Jan 22 2021 at 22:08):

@Jordan Brown When are you free on Mondays?

Jordan Brown (Jan 23 2021 at 01:45):

I should be free 10-12, 3-5, and after 6

Thomas Browning (Jan 23 2021 at 03:46):

I'm free 10-12 on mondays. Does that work for you @Patrick Lutz ?

Thomas Browning (Jan 23 2021 at 08:41):

@Patrick Lutz I've started a new branch (https://github.com/leanprover-community/mathlib/compare/polynomial_galois_group) for the polynomial_galois_group PR. It depends on #5845.
I think that I got most of the relevant results from the abel-ruffini branch. Feel free to make changes.

Patrick Lutz (Jan 23 2021 at 17:29):

@Thomas Browning 10-12 on Mondays should work for me in future weeks, but not next week (because I don't think I should move my office hours two days before they are supposed to happen)

Thomas Browning (Jan 23 2021 at 18:00):

Sure, so shall we meet at 1pm this monday and at 10am on following mondays?

Patrick Lutz (Jan 23 2021 at 18:13):

that's okay with me

Thomas Browning (Jan 23 2021 at 20:10):

I've opened a PR (#5861)

Thomas Browning (Feb 01 2021 at 18:09):

@Patrick Lutz

Jordan Brown (Mar 01 2021 at 05:37):

There's a planned power outage in my area tomorrow morning, so I might not have internet; if I can't come to the meeting
, I will try to say something about where I am in the stream

Jordan Brown (Mar 22 2021 at 00:00):

@Thomas Browning can we move our meeting later this week? I haven't had much time to do Lean since Monday, but I should have a lot of time to work on it over the next few days

Thomas Browning (Mar 22 2021 at 00:39):

@Jordan Brown Sure, I'm basically free whenever. Just let me know when you want to meet.

Jordan Brown (Mar 25 2021 at 03:37):

@Thomas Browning how about Friday sometime around noon? Are you free then?

Thomas Browning (Mar 25 2021 at 03:57):

I won't be (2nd shot). I'll probably be back by 8pm (I'm biking, and it could be 3-4 hours each way), if you want to meet then. If not, I'm free tomorrow (except 2pm-3pm) and at various times on the weekend (at least Saturday evening and Sunday afternoon).

Jordan Brown (Mar 26 2021 at 02:01):

@Thomas Browning Hmm, okay. Those times are not great for me; perhaps we should just meet at the usual time Monday.

Thomas Browning (Mar 26 2021 at 02:39):

Sounds good.

Last updated: Dec 20 2023 at 11:08 UTC