London, England

Stream: Geographic locality

[Kevin Buzzard]

The Xena Project meets every Thursday evening during Imperial's term (early Oct to mid-Dec, early Jan to mid-March, mid-April to end of June) in the maths department at Imperial College London in South Kensington (although if you're not attached to Imperial there will be a few card-only locked doors you'll have to negotiate; ping me).

[Stefano]

Kevin Buzzard said:

The Xena Project meets every Thursday evening during Imperial's term (early Oct to mid-Dec, early Jan to mid-March, mid-April to end of June) in the maths department at Imperial College London in South Kensington (although if you're not attached to Imperial there will be a few card-only locked doors you'll have to negotiate; ping me).

Hi,
I'm based in London too (sort of, at least for work). Also studying (part-time) Mathematics at Birkbeck.
@Kevin Buzzard is the Xena meetup still going on?

[Kevin Buzzard]

Yes although it's very quiet right now because it's post exams and most students have gone home

[Alex J. Best]

Hi, I've just moved to London (KCL) :smile:

[Eric Rodriguez]

yoo! I'm doing my masters' there, i'll come say hi at some point ^^

[Daniel Rogozin]

I'm going to do a PhD at UCL :hi:

[Kevin Buzzard]

Xena meets on Thursdays at Imperial during term times 5-8pm, and London Learning Lean is before that at 4-5.

[Daniel Rogozin]

South Kensington Campus?

[Daniel Rogozin]

I think I would participate in those meets starting next Thursday.

Btw, how do strike actions affect Imperial working hours and, subsequently, Xena meets? My UCL colleagues, for example, are going to participate in strike actions this month and cancel some events.

[Kevin Buzzard]

They won't be affected.

[Daniel Rogozin]

@Kevin Buzzard

Do I need any permission to enter the Imperial campus to join Xena meets?

At UCL, the guards tend to stop people without a scheduled appointment

[Kevin Buzzard]

There are no guards at Imperial. Perhaps we should take this discussion to DMs.

[Geoffrey Irving]

I'm in London and between jobs at the moment, and one of the things I will be doing during my break is continuing Mandelbrot set fiddlings (https://github.com/girving/ray). I'd be fun to catch up with other Lean folk, whether just to have lunch chats or to occasionally work near others to be able to absorb wisdom.

[Geoffrey Irving]

@Alex J. Best (who replied in the other thread): Lunch sometime? Details over DM?

[Geoffrey Irving]

@Kevin Buzzard Are the Xena Thursday 5-8 p.m. meetings still going?

[Eric Rodriguez]

Xena will be running, I'm sure, from some point soon - note it's usually mostly students from undergrad to PhD there

[Paul Lezeau]

I usually attend Xena with @Calle Sönne, and @Eric Rodriguez mentionned he'd be joining at some point!

[Paul Lezeau]

@Geoffrey Irving I'd be up for joining you guys!

[Eric Rodriguez]

Me too :)

[Geoffrey Irving]

Do you mean for lunch or Xena? I'm up for either. If lunch, maybe early next week?

[Eric Rodriguez]

Early next week suits me!

[Kevin Buzzard]

Xena starts again on 11th btw (but I guess I'll be watching Lean Together for the first bit)

[awalterschulze]

We used to do Coq, but now we do Lean. Would be great to meet https://www.meetup.com/london-tydd/events/298607045/

[Kevin Buzzard]

Can you move your message to the "London, England" thread linked to above?

[Notification Bot]

Alex J. Best has marked this topic as unresolved.

[Notification Bot]

2 messages were moved here from #Geographic locality > ✔ London, UK by Alex J. Best.

[Alex J. Best]

Kevin Buzzard said:

Can you move your message to the "London, England" thread linked to above?

Btw Kevin anyone can more messages within a stream (I think). So I took the liberty of doing just that here.

[Geoffrey Irving]

Is Xena on tomorrow? Kevin’s talk is streaming at 5, and I’ll also be curious to watch that; not sure if those two things should connect.

[Geoffrey Irving]

I suppose an alternative option is actually going to Cambridge…

[Kevin Buzzard]

I will be giving the talk in Huxley 139 in front of an audience at Imperial, and live streaming to Cambridge. After that we'll all wander up three flights of stairs and have the Xena meeting 6-8pm.

[Geoffrey Irving]

Great, I’ll join in.

[Yaël Dillies]

Feel free to come to Cambridge one of these days, though. There's a few of us there and it would be great to meet you. :smile:

[Geoffrey Irving]

I will take you up on that! Gone next week, but I’ll ping some time after that.

[Paul Lezeau]

Would anyone in London be up for another small meetup sometime soon?

[Kim Morrison]

Unexpectedly in London for 24 hours, thanks BA! :-)

[Eric Rodriguez]

Sadly not here for a couple days!

[Paul Lezeau]

Would anyone in be up for a small meetup in London sometime soon? We could do lunch/find a coffee shop to work together if anyone's interested:)

[Yaël Dillies]

I should be there in two-ish weeks, if that's not too far away

[Calle Sönne]

Yes lets do it!

[Eric Rodriguez]

absolutely!

[Alex J. Best]

Nice idea, I'm down!

[Stefano]

Great idea. I’m in!

[Paul Lezeau]

Awesome! Two-ish weeks from now is also perfect for me. How about, tentatively, Saturday 5th?

[Yaël Dillies]

Unclear whether I'll be there yet

[Anand Rao Tadipatri]

I'd be up for this too!

[Luisa Cicolini]

me too!

[Paul Lezeau]

I've created a separate group to organise this to avoid spamming this thread. If anyone else wants to join, message me and I'll add you:)

[Andrew Yang]

I arrived here a week ago and I'll be here for the foreseeable future as a PhD student of Kevin. Excited to meet any Lean people here!

[Paul Lezeau]

For people who are interested in joining the London Lean meetup this weekend, we'll be meeting at 12.30 on Saturday here.
Please react to this message before lunchtime tomorrow (04/10) so I can make a reservation (I'll need to know roughly how many people are planning to show up) :smiley:

[Yaël Dillies]

With double the room so that you can get the computers out? :grinning:

[Eric Wieser]

Yeah, I'm curious what the computer-compatible plan is!

[Paul Lezeau]

The idea I was suggesting was lunch and then finding a cafe to sit down for a few hours, but feel free to suggest if you have better ideas :grinning_face_with_smiling_eyes:

[Bhavik Mehta]

First to take out their laptop pays for everyone's food

[Kevin Buzzard]

Ha ha that reminds me of the dinner after CPP where Anand Rao pulled out his laptop and put it on the table during the meal and started talking to Jannis about aesop :-)

[Paul Lezeau]

Ok so I have looked into booking a table, and it appears to do so I would have to pay a £15/person deposit, which is not ideal!
I suggest we try to get a table there tomorrow, and find another nearby restaurant (there are many) if that doesn't work out.

[Eric Wieser]

We accept bookings only for lunch or dinner meals.  Walk-ins are welcome for coffees and drinks only.

I don't think the "try" plan will work

[Paul Lezeau]

Ok backup plan: I've made a reservation at the Pizza Express on Euston Road (full address: Clifton House, 93-95 Euston Road) at 12.30.
After lunch we can either find somewhere to chat in the British library, or go to the common room at the UCL math department (Calle and I have card access)

[Matthew Eric]

I was really excited to join y'all this saturday but I've come down with a bit of a cold and don't want to infect anyone. I hope we do another meetup soon!

[Eric Wieser]

I'm across the street in the sun, fixing some merge conflicts

[Calle Sönne]

What sun :thinking:

[Paul Lezeau]

We're in

[Paul Lezeau]

(so you can fix merge conflicts at the table now;))

[Kevin Buzzard]

I've just woken up lol

[Kevin Buzzard]

I'll be there in 15

[Dominic Steinitz]

Great to meet everyone yesterday :smile: Was someone going to post the account details so I can pay my fair share for lunch?

[Eric Wieser]

I forwarded Alex's message to you privately

[Sidharth Hariharan]

Can you forward it to me as well?

[Dominic Steinitz]

Some of us discussed the law of the excluded middle. This is a very entertaining talk on it: Andrej Bauer: Constructive Mathematics - How to not believe in the Law of Excluded Middle.

[Paul Lezeau]

/poll People seemed to be quite interested in doing more meetups, and I think the weekend of the 19th could work quite well. What would people prefer? (feel free to add more options!)
Saturday afternoon (e.g. Lunch + working together)
Saturday evening (e.g. work together + dinner)
Sunday afternoon (e.g. Lunch + working together)
Sunday evening (e.g. work together + dinner)

[Yaël Dillies]

I will be in Imperial for three months starting from this afternoon! Anyone around today?

[Calle Sönne]

I wasn't around today, but will be in the rest of the days this week!

[Paul Lezeau]

Seems like Saturday evening is the best fit! We could start in the afternoon at UCL and then go to get dinner in the area.
@Alex J. Best suggested Franco Manca - we could go to the one near Russel Square (4 Bernard St, Russell Sq)

[Paul Lezeau]

I'll call tomorrow to make a reservation. If anyone voted but can't make it in the end/didn't vote but would like to be added, please let me know quickly so have a rough idea of how many people will be coming:)

[David Ang]

I'll be there for the work together but not the dinner :)

[Eric Rodriguez]

are we hoping to book a UCL room or?

[Paul Lezeau]

I'm not sure we can book rooms for the weekend.

[Paul Lezeau]

Ok so let's say we can meet up around 4pm next the the UCL student union entrance.

[Andrew Yang]

Have people arrived yet?

[Paul Lezeau]

When people arrive, just DM me and I can let you in:)

[Alex J. Best]

I'm arriving now (1 min away)

[David Ang]

An option in contrast to the common room is Room 416 on the 4th floor, which has a huge whiteboard and many sockets.

[Yaël Dillies]

Currently in the tube. Will arrive in 35min.

[Paul Lezeau]

Anyone up for a meetup this weekend? E.g. pub trip or something like that.

[Alex J. Best]

Or Friday evening if it's a pub meetup?

[Paul Lezeau]

Friday sounds good to me!

[Markus Himmel]

I'm in London this week and would love to come, but unfortunately Friday evening doesn't work for me. Wednesday, Thursday or Saturday evening would all be great.

[Yaël Dillies]

I am still a bit sick, so I would rather not meet today. What about saturday?

[Kevin Buzzard]

Just to comment that I was out last Sat in central London and it was completely bonkers, people queueing to get into massively crowded pubs etc, super-busy. So a less central place might be a good idea.

[Kevin Buzzard]

For example https://maps.app.goo.gl/bUB1bWmR34LNj2ts7 is a big pub not in Zone 1 (a Spoons) where seating would be unproblematic.

[Paul Lezeau]

Kevin Buzzard said:

For example https://maps.app.goo.gl/bUB1bWmR34LNj2ts7 is a big pub not in Zone 1 (a Spoons) where seating would be unproblematic.

Looks good to me!

[Kevin Buzzard]

So Saturday night in the Coronet (the link above)? That works for me. What time? 8pm? It's about 5 minutes' walk from Holloway Road tube (Picadilly line) BTW. PS judging by the google reviews it's no longer a Spoons (but it's still a very big pub not in Zone 1)

[Andrew Yang]

Will there be a work-together part in the afternoon?

[Yaël Dillies]

That would be great!

[Kevin Buzzard]

Well I'm not sure I'd recommend the Coronet for that! Sticky tables, no WiFi, drunk people. There's Coffee Zee just down the road from the Coronet where people can work (decent Wifi, clean tables, no drunk people).

[Kevin Buzzard]

That closes at 5 but there's a Costa opposite if people don't want to start drinking at 5

[Kevin Buzzard]

I could be at Coffee Zee for 2pm

[Andrew Yang]

So what's the plan? I could also be at Coffee Zee at 2.

[Kevin Buzzard]

Let's do Zee at 2, and Coronet at 8, and there's McDonalds and a pizza place and Costa and many other places to eat in the neighbourhood in between. I might have to disappear in the middle because of family matters but I am pretty sure I can do those two times at least. The Coronet is open all day IIRC :-)

[Yaël Dillies]

A friend and I will be at Zee at 14:0ε

[Paul Lezeau]

Should be able to join for the evening.

[Kevin Buzzard]

I'm there

[Kevin Buzzard]

Lol so is Jeremy Corbyn

[Markus Himmel]

I'll also be there at 8.

[Eric Wieser]

Unfortunately the thameslink trains aren't running where I need them to today, so I won't be able to make it

[Eric Rodriguez]

For any other early people I'm at the indiebeer, just near the coronet :) they have mulled wine!

[Alex J. Best]

Eric superposition collapsed

[Andrew Yang]

We are in the coronet now.

[Kevin Buzzard]

I think I'd rather be at indie beer though, it's stupid loud here

[Kevin Buzzard]

@Eric Rodriguez is there space for eight of us?

[Kevin Buzzard]

Ok we're at indie beer on the holloway road, very near the coronet

[Rita Ahmadi]

Hello, Are there any Thursday seminars/meet-ups at Imperial between Jan-March 2025? Thank You!

[Kevin Buzzard]

Yes, there's a weekly meeting Thursdays 5-8pm at Imperial College, the first one this term will be 9th Jan

[Kevin Buzzard]

They're in the computer room on the 4th floor in the Huxley building

[Rita Ahmadi]

Is the Computer room 410?

[Kevin Buzzard]

No it's the much bigger one, but I know that you found it because I saw you there :-) Thanks for coming!

[Paul Lezeau]

Would anyone be interested in another Lean meetup on Saturday?

[Paul Lezeau]

How about co-working at the same café as last time and then a drink at that nice beer place we went to?

[Kevin Buzzard]

Yeah that works for me, coffee Zee and indie beer on Holloway road. What time?

[Paul Lezeau]

How about 4pm?

[Kevin Buzzard]

Well just to warn you that Arsenal are at home to Aston Villa kick-off 5:30-7:30pm on Sat so Holloway Road tube will be shut between 3:30 and 5:45, and also between 7pm and 10pm (all times approx but I've been maximally pessimistic with these predictions). The nearest tubes to Coffee Zee during these times are Highbury and Islington, and Caledonian Road (both about 15-20 minutes walk away). In short 3pm would be more convenient ;-)

[Paul Lezeau]

Good point, 3pm it is in that case!

[Dominic Steinitz]

Sadly I can't join this time

[Kevin Buzzard]

Dominic, you should meet Heather at some point, she's in London now and is an expert in lean manifolds

[Kevin Buzzard]

We've left the coffeeshop and we'll be at Indiebeer https://indiebeer.co.uk/ from 7pm

[Dominic Steinitz]

Kevin Buzzard said:

Dominic, you should meet Heather at some point, she's in London now and is an expert in lean manifolds

I would love to meet Heather. I am going to SOAS tomorrow evening and could pop in beforehand if it were convenient for Heather and you.

[Rebecca Bellovin]

I'm going to be in London for much of the spring (hopefully starting Feb 2), and I'd be happy to come to any future meetups

[Paul Lezeau]

How about another meetup on the 8th?

[Dan Abramov]

I live in London, would love to go to meetups / study groups / any events, really. My schedule is relatively free. (I will be mostly traveling for the few next months though.)

[Dan Abramov]

Are the 5pm Imperial College meetings still active (seems like yes according to this thread)? Can I come by (tomorrow today)? I'm assuming it's open to non-students (how do I get in)?

[Kevin Buzzard]

Yes you'd be welcome. They're on Thursdays during term time (which is now) 5-8pm at Imperial College, in the Huxley building (maths department) in the big computer room on the 4th floor just by the elevators. I'm the guy with the silly trousers

[Yaël Dillies]

And I'm the person with the yellow clothes :smile:

[Kevin Buzzard]

As some locals will know, for the last few months Richard Hill and I have been running in person informal London Learning Lean meetings, alternating between UCL and Imperial, with a frequency of about one per month. The format is something we've been experimenting with and we now have something which we're pretty happy about: the sessions are about 90 minutes long and anyone can stand up and give a 10 minute chat on something they've been thinking about, which could be a discussion of completed or ongoing work. We thought we'd now go public; the next meeting is a week on Friday at Imperial.

When: Friday 28th Feb 4-6pm (refreshments at 4, presentations start 4:30, bar at 6pm)
Where: Huxley Building room 341, Imperial College London

Anyone considering presenting: you don't have to prepare pdf slides or anything, people just plug in their laptop and display Lean code and chat about it and write on a whiteboard if necessary.

[Kevin Buzzard]

Thanks to all the people who came yesterday! I was delighted to see so many people and it was great that a bunch of Lean enthusiasts got to meet each other (and I learnt facts such as "Jovan Gerbscheid lives in the UK") .

[Yaël Dillies]

People coming to Xena today: We're not in the usual corner of the MLC, but the far right one, with the long alignment of computers

[Kevin Buzzard]

The next London Learning Lean is on Friday 28th March 3-5pm (note time change) at the London Institute for Mathematical Sciences, just above the Royal Institution (map, nearest tube Picadilly Circus). Feel free to bring a laptop and something Lean-related to say which lasts <= 10 minutes and which you don't have to prepare any slides for. Or just watch.

[Bhavik Mehta]

(I think nearest tube is green park!)

[Dominic Steinitz]

I could talk about my work on the Möbius band as a G-bundle but 10 minutes to explain what a G-bundle is might be challenging let alone talking about the Lean implementation.

[Kevin Buzzard]

Assume people know what a G-bundle is!

[Pim Otte]

I happen to be in town, so I'll join this afternoon:) I don't have my laptop with me, but if I could borrow one I could tell a bit about Tutte's theorem

[Bhavik Mehta]

Here's some general information about where to go: Follow Kevin's link above, then when you're there, look for the entrance to the RI - it says something about a museum and free water. Go in that door, then ask for LIMS at the reception or just go up the stairs you'll see, up two floors. You'll see a big brown door, which is the way into LIMS. Feel free to DM me if you're stuck somewhere! They've given us an event page too

[Bhavik Mehta]

Some of us are now downstairs in the king's head

[Dominic Steinitz]

It was a very fun afternoon - thanks for organising - I made Möbius into a (draft) PR: https://github.com/leanprover-community/mathlib4/pull/23426/files. I think there was some discussion of adding it to a collection of examples. I doubt it should actually go into Mathlib (well maybe the definition of a G-bundle).

[Kevin Buzzard]

We're trying a pattern of "last Friday in the month" for London Learning Lean. So the next one will be on Friday 25th April (a week tomorrow), at UCL, with talks from 3:30 to 5 (and refreshments 3-3:30)

Last time there were a couple of unhappy people who came to LLL with ten-minute talks prepared but they weren't called on. So this time we're giving people the opportunity to let me know beforehand if they want to reserve a slot. Bhavik also suggested that instead of 10 minutes for talks and 5 minutes for questions we should have 9 minutes for talks and 1 minute for questions, so we can increase the number of talks (because people can ask their questions down the pub afterwards). Whether or not this becomes a reality will probably depend on how many people contact me asking to reserve a ten minute slot!

[Kevin Buzzard]

LLL update from Richard Hill:

---

The meeting is in the Harrie Massey lecture theatre. This room is on the ground floor of the building containing the maths department, near to the back entrance.

Time still 3:30-5pm Friday 25th April.

If you'd like to use the coffee machine in the maths department 6th floor common room from 3pm then please bring a cup.

[Kevin Buzzard]

I'm in the Caffe Nero at Euston Station (what3words shell.warm.jukebox ) , entrance from the path south of the cafe)