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)

[Kevin Buzzard]

Next London Learning Lean is in 2 weeks (and 2 hours); indeed right now we're sticking with the "last Friday in the month" algorithm. It's Friday 30th May at Imperial College London in Huxley 140 (the basement of the building), luxurious refreshments just outside the room 3-3:30 (cups will be provided on this occasion), 10-minute talks 3:30-5pm. All welcome, you don't have to speak, let me know if you do want to speak and want to reserve a slot, social at Imperial student union bar afterwards.

[Dominic Steinitz]

Is this still on?

[Andrew Yang]

Yes. Allegedly there are even nice cakes.

[Eric Wieser]

Info to get there is https://www.imperial.ac.uk/engineering/study/current/teaching-spaces/huxley-140/, I assume?

[Notification Bot]

12 messages were moved from this topic to #mathlib4 > Manifold structure on Moebius strip by Kevin Buzzard.

[Joseph Tooby-Smith]

I will be in London next Friday (13th June) late afternoon if anyone is around and wants to meet up? (I'm Flying in on the morning).

[Eric Wieser]

A bunch of people might be coming back to an airport from Big Proof in Cambridge that evening

[Paul Lezeau]

I’d be happy to meet up!

[Kevin Buzzard]

Or just coming back to London because they live there :-)

[Joseph Tooby-Smith]

If there is a time and place which would allow more people to join I'm somewhat flexible. Though know it may be the last thing people want after a conference :). Can't be flexible with the day though :( , as making a very quick visit to the UK.

[Paul Lezeau]

@Joseph Tooby-Smith and I will be meeting up at Mable’s Tavern (near King’s Cross) at 6.30 tomorrow on Friday if anyone wants to join!

[Joseph Tooby-Smith]

@Paul Lezeau Friday, right? :)

[Paul Lezeau]

Absolutely!

[Kevin Buzzard]

Next LLL is back at LIMS in central London on the last Friday in June (June 27th). Because of the mathlib community meeting at 3pm London time we've decided to delay the start, so it's informal social 330-4 and ten-minute talks 4-5:30 before venturing out into Mayfair for drinks. If you want to reserve a ten minute slot then DM me letting me know, or else try your luck, show up with a laptop and enjoy their Hagoromo!

[Kevin Buzzard]

• London Institute for Mathematical Sciences
• Royal Institution
• 21 Albemarle St
• London W1S 4BS

[Dominic Steinitz]

Sadly I won't be able to join today.

[Chris Birkbeck]

same :(

[Kevin Buzzard]

There will be plenty there, don't worry :-)

[Calle Sönne]

Will anyone be going there from imperial? I know at least me and @Yaël Dillies will be

[Yaël Dillies]

Yaël Dillies, the very famous Imperial PhD student :disguised_face:

[Kevin Buzzard]

I will be leaving Imperial at 3ish but I might take the bus because there's a mathlib community meeting which I won't be able to watch on the tube

[Eric Wieser]

If we arrive early is there somewhere we can join the community meeting from?

[Kevin Buzzard]

Ask Yang, he might be able to set something up

[Kevin Buzzard]

(bus very slow, will be there at 4 on the dot)

[Paul Lezeau]

Would people in London be up for a coffee plus co-working either this Saturday or the next?

[Paul Lezeau]

@Edison Xie how about the 19th?

[Edison Xie]

I’m down, where do you have in mind and should we have dinner together after that?

[Edison Xie]

@Paul Lezeau

[Kevin Buzzard]

I'm out of town for the next two weeks by the way, so I can't do meet-ups and also there's going to be no LLL at the end of July

[Paul Lezeau]

Edison Xie said:

I’m down, where do you have in mind and should we have dinner together after that?

Let me find a place and I’ll post it here! And definitely up for dinner after that:)

[Paul Lezeau]

For people who wanted to meet up tomorrow, how about the WatchHouse café (near Tower Bridge) at 5.30-ish?

[Andrew Yang]

I just landed in London. Is this thing today (19th) or tomorrow (20th)? (I can't tell because of timezone issues)

[Eric Rodriguez]

actually it was yesterday

[Eric Rodriguez]

jk it's today 19th

[Paul Lezeau]

I’m running a little late!

[Andrew Yang]

There are currently only three imperial people here right now as far as I can tell.

[Michał Mrugała]

I’ll join a little later

[Andrew Yang]

They said they are closing at 6 though

[Andrew Yang]

We have moved to the Starbucks nearby.

[Kevin Buzzard]

London Learning Lean update: Richard and I have decided to skip August and have the next two LLLs at Imperial last Fri in Sept and UCL last Fri in Oct.

[Rado Kirov]

I am visiting London for 5 days soon - Mon, Aug 18 to Fri, Aug 22. Would love to grab coffee with some of the Lean experts in the city. Pretty flexible timewise, just sightseeing with family most of the days.

[Kevin Buzzard]

There will be a bunch of us doing lean at Imperial on the afternoon of Thursday 21st if that works for you

[Rado Kirov]

Perfect! Will ping you in DMs for time and place a couple of days before.

[Rado Kirov]

It was great meeting everyone doing Lean at Imperial today. Thank you for having me over!

[Stefan Zetzsche]

The latest edition of the South of England Regional Programming Languages Seminar (S-REPLS) will be held at Amazon UK's headquarter in London on 29th October 2025.

Please register via https://aws-experience.com/emea/uki/e/70859/s-repls if you would like to attend.

If you would like to give a talk, please send a talk proposal to Stefan Zetzsche stefanze@amazon.co.uk by mid September. Talks are typically 20-30 minutes long and should be given in person. We invite proposals for talks on any topic related to programming languages. The meeting will be informal, so talks on any related topic at any stage of development (from work submitted for publication to mature projects) are welcome.

[Kevin Buzzard]

London Learning Lean is back, this time at Imperial College London on Friday 26th September, with refreshments 3:30-4 and then ten-minute talks 4-5:30 and then student union bar (assuming it's open -- Imperial will still be student-free!). Room to be announced shortly. Room is Huxley 340

[Dominic Steinitz]

Kevin Buzzard said:

London Learning Lean is back, this time at Imperial College London on Friday 26th September, with refreshments 3:30-4 and then ten-minute talks 4-5:30 and then student union bar (assuming it's open -- Imperial will still be student-free!). Room to be announced shortly. Room is Huxley 340

Sadly I can't join you today.

[Sidharth Hariharan]

Hi everyone! I'm a former Imperial student now doing a PhD at CMU. ("Former" - I was there till June :D)
Anyway, I'm going to be in London from 7 to 13 October (that's next Tuesday-the Monday after). If people are around, it would be nice to meet! I'm not available on the 8th (Wednesday), the 9th (Thursday), or the afternoon of the 11th (Saturday), but other days are looking alright for now

[Kevin Buzzard]

Term started on Monday so I guess Xena will start again on Thursdays 5-8pm if you want to swing round and say hi! I haven't seen you since...Leiden two weeks ago I guess ;-)

[Sidharth Hariharan]

I’d love to, but I’m in Cambridge that evening to give a talk about the sphere packing project at their formalisation seminar. I will be around campus that afternoon though.
Been ages though, for sure… :D

[Edison Xie]

Sidharth Hariharan said:

Hi everyone! I'm a former Imperial student now doing a PhD at CMU. ("Former" - I was there till June :D)
Anyway, I'm going to be in London from 7 to 13 October (that's next Tuesday-the Monday after). If people are around, it would be nice to meet! I'm not available on the 8th (Wednesday), the 9th (Thursday), or the afternoon of the 11th (Saturday), but other days are looking alright for now

welcome back! we should meet :-)

[Paul Lezeau]

I'd also be down to meet up!

[Eric Rodriguez]

me too :)

[Andrew Yang]

Maybe something tomorrow (Sunday)?

[Edison Xie]

Andrew Yang said:

Maybe something tomorrow (Sunday)?

I think Sid meant next Sunday but if anyone wants to meet tmr I'm down as well :-)

[Andrew Yang]

Oh I misread. :'( I'll ask again next Saturday if nothing happens by then.

[Sidharth Hariharan]

How about lunch next Sunday?

[Sidharth Hariharan]

I'd also be free on Saturday evening if people prefer that. Could maybe meet somewhere in Covent Garden - I'm very open to suggestions

[Paul Lezeau]

Sunday lunch works pretty well for me!

[Kevin Buzzard]

My family are away so I could also do next weekend

[Bhavik Mehta]

My preference from those two is Saturday evening

[Andrew Yang]

/poll Let's do a quick poll then
Saturday evening
Sunday noon
Sunday evening

[Kevin Buzzard]

This is 11th/12th right? I'm flexible

[Sidharth Hariharan]

Unfortunately something has come up for Saturday evening - but Sunday is still completely open! Sorry for the confusion.

[Sidharth Hariharan]

Shall we do Sunday evening then? How about the Pizza Express near St Paul's?

[Sidharth Hariharan]

Say 18:30

[Paul Lezeau]

Sounds good!

[Chris Birkbeck]

Is anyone here yet?

[Kenny Lau]

i’ll be a bit late

[Yaël Dillies]

Sorry, we had a very captivating cosmology cohomology livecoding session

[Sidharth Hariharan]

Had a great time - thanks for coming everyone! I’ll be sure to message here the next time I’m in town

[Kevin Buzzard]

Looks like LLL will be at UCL on 31st Oct, late afternoon, will post more when UCL gets back to me.

There's also this coming up at Imperial:

Apple Formal Verification Tech Talk

Thursday, 23 October 2025
2:15 pm - 3:45 pm (BST)

EEE Building, Room 508, 5th Floor

Imperial College London South Kensington Campus SW7 2AZ

Register

This talk introduces formal hardware verification to students across mathematics, computing and engineering disciplines, bridging theoretical foundations with practical industry applications.

We’ll explore how mathematical proof techniques ensure the correctness of complex hardware systems, from Apple’s cutting-edge System-on-Chip designs to specialised mathematical computation units.We’ll look at how hardware verification problems transform from code into Boolean functions and propositional logic, demonstrating through concrete examples how formal methods complement and extend simulation to deliver rigorous bug detection and correctness proofs essential for modern silicon.

There will be the opportunity for questions, and to discuss internship opportunities for 2026 with leading Apple engineers.

[Kevin Buzzard]

The next LLL at UCL is Friday 31st October in
B20 Jevons lecture theatre, Drayton House.

This is across the road from the maths department.

We'll start at a slightly later time:

• 4-4:30 refreshments,

• 4:30-6, informal ten-minute talks.

[Kevin Buzzard]

LLL tomorrow! Refreshments will be 4pm-4:30pm in room 502 in the UCL Mathematics department, and then we'll leave for Drayton House with LLL 430-6. I will also be giving a generic Kevin intro to Lean talk 6-7 suitable for UCL undergrads in the same venue.

[Eric Rodriguez]

Where did people head afterwards? [Had to run off for a call]

[Chris Birkbeck]

In Phineas

[Chris Birkbeck]

4th floor of maths

[Kevin Buzzard]

London Learning Lean is happening, as usual, on the last Friday of the month, which is a week today, 28th Nov 3-5pm at Imperial College London in room Huxley 642. Refreshments 3-330 and then 10 minute talks 330-5 (let me know if you want to give one, or just show up and take your chances) and then we hit the bar.

Unsurprisingly there will be no LLL on Boxing day, so the next one after this will be in Jan.