Edinburgh, UK

Stream: Geographic locality

[Andrés Goens]

I've relocated to Edinburgh (at UoE) and see there's no Stream, so I'm starting one here. Who knows, maybe some of the Agda people decide to wander over to the Lean 'dark side' :wink:

[Ramon Fernandez Mir]

Hi @Andrés Goens ! I'm also at UoE. I'm doing a PhD and using Lean for some of it. We should meet up!

[Marcus Rossel]

@Ramon Fernandez Mir What are you working on?

[Ramon Fernandez Mir]

@Marcus Rossel Hybrid systems verification! And right now I'm using Lean to check results from convex optimisation solvers :-) I can explain in more detail if you're interested

[Andrés Goens]

@Ramon Fernandez Mir that's great! definitely, let's meet up!

[Jon Eugster]

I'm also in Edinburgh :wave: . I'm doing a PhD in alg.geo so not Lean related, but I've always been interested in Lean, had some Lean projects I've been working on, and I'm still thinking about doing more Lean in the future.

[Kevin Buzzard]

Jon you should get on the lean alg geom bandwagon! We're slowly moving through chapters 2 and 3 of Hartshorne.

[Jon Eugster]

That'd be cool. How do I get involved in that?

[Kevin Buzzard]

You could start by taking a look at the algebraic_geometry directory in mathlib, and there might even be a github project running for the chapter 2 stuff. The chapter 3 stuff is happening in LTE mostly.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/projects/13

[Andrés Goens]

Hey @Jon Eugster ! @Ramon Fernandez Mir and I were thinking of getting lunch on Monday at 13:00 around campus, would you want to join us?

[Jon Eugster]

I'd love to. Is campus JCMB? Because I have a tutorial at 2pm there.

[Andrés Goens]

I guess I meant around George Square. Happy to choose somewhere in the middle if that works for @Ramon Fernandez Mir too though

[Andrés Goens]

We're going to try to revive these lunches, @Jon Eugster are you still around? @Ramon Fernández Mir and I were thinking of trying this Thursday at 12:30, we could try MF1 at the Informatics Forum? (Also CCing @Siddharth Bhat @Fehr Mathieu @Tobias Grosser @Orestis Melkonian )

[Tobias Grosser]

@Chris Hughes also just today joined us in Edinburgh.

[Kevin Buzzard]

He knows a thing or two about Lean ;-)

[Jon Eugster]

I'm in Düsseldorf now :)

[Ramon Fernández Mir]

Reminder: there is another Lean lunch this Thursday (27th) at 12:30!

[Ramon Fernández Mir]

Lean lunch happening again today at 12:30 at the Informatics forum MF1! @Andrés Goens @Chris Hughes @Siddharth Bhat @Fehr Mathieu @Tobias Grosser @Orestis Melkonian @Paul Jackson

[Tobias Grosser]

Traveling atm.

[Patrick Kinnear]

Hi Edinburgh Lean people!

David Jordan and I are based in the School of Maths and planning to run a pilot course this semester on Lean aimed at graduate students in algebra, topology, geometry, category theory etc. This is part of the group's aim of delivering some form of programming relevant to grad students in algebra and related fields. We though Lean might be more interesting than just going over a computer algebra system, and it might be more of a level starting point since Lean could be quite different to the sorts of languages the students are most likely to have met before.

David and I are just starting out learning Lean ourselves, so the course will be very student led and collaborative. A reasonable goal for the course would be that participants learn how to interact with the Lean environment, and to access the existing library of mathematics, and that by the end we are able to venture into proving new theorems (i.e. translating known theorems from our discipline) into the library. So we will probably start with some tutorials and then move more towards some project-based work.

We are still at the stage of planning how exactly the course will run. I wanted to touch base here since I'm aware, via Jon Eugster, that there are quite a few Lean experts mainly based in Informatics. Let me know if you have any thoughts, suggestions for teaching, project ideas, or any other interest in this pilot course.

Thanks,

Patrick

[Ruben Van de Velde]

There's also a #Lean for teaching stream you might want to subscribe to if you haven't yet

[Jeremy Avigad]

Hi, Patrick. Last semester, I taught an undergraduate class on formalizing mathematics at Carnegie Mellon. We spent the first half of the course making a quick run through the core parts of Mathematics in Lean, after which students worked mainly on projects of their choosing. I'd be happy to answer questions.

[Chris Hughes]

Hi. I'm at Edinburgh and I'd love to help out. I spent summer of 2018 hanging around in a room full of mathematicians answering Lean questions and it was good fun and I'd love to do it again.

[Andrés Goens]

We were trying to do some Lean lunches with @Ramon Fernández Mir (and @Chris Hughes, @Siddharth Bhat and @Tobias Grosser ). Maybe we could do one of those as well with you @Patrick Kinnear and David Jordan. I'd also be very curious about that course and happy to help out if I can.

[Siddharth Bhat]

I'm at Edinburgh as well, and I would be very happy to be involved with running the course!

[Tobias Grosser]

Yes, getting a lean lunch with @Patrick Kinnear to discuss the lean in math sounds like an excellent idea. I would love to hear more about the plans.

[Kevin Buzzard]

Chris Sangwin is interested in lean in mathematics education, and Paola Iannone is also moving to Edinburgh or is perhaps there already. You've got quite a crowd up there!

[Ramon Fernández Mir]

Andrés Goens said:

We were trying to do some Lean lunches with Ramon Fernández Mir (and Chris Hughes, Siddharth Bhat and Tobias Grosser ). Maybe we could do one of those as well with you Patrick Kinnear and David Jordan. I'd also be very curious about that course and happy to help out if I can.

Yes, let's restart them this semester! What about Thursday next week at 12 in MF1? Does that work for you @Patrick Kinnear and David Jordan?

[Andrés Goens]

@Patrick Kinnear for clarification: MF1 is in the Informatics Forum

[Patrick Kinnear]

Jeremy Avigad said:

Hi, Patrick. Last semester, I taught an undergraduate class on formalizing mathematics at Carnegie Mellon. We spent the first half of the course making a quick run through the core parts of Mathematics in Lean, after which students worked mainly on projects of their choosing. I'd be happy to answer questions.

Thanks Jeremy! I take it you are based at Carnegie Mellon and not here in Edinburgh (i.e. there's no chance we'll see you in person)? I'd love to ask you some more questions about your course, though first I think David and I need to have a chat about exactly what we want to get out of ours. I'll keep in touch!

[Patrick Kinnear]

Ramon Fernández Mir said:

Andrés Goens said:

We were trying to do some Lean lunches with Ramon Fernández Mir (and Chris Hughes, Siddharth Bhat and Tobias Grosser ). Maybe we could do one of those as well with you Patrick Kinnear and David Jordan. I'd also be very curious about that course and happy to help out if I can.

Yes, let's restart them this semester! What about Thursday next week at 12 in MF1? Does that work for you Patrick Kinnear and David Jordan?

Thanks guys, yes I'd love to join you for lunch next Thursday at 12 in the Inf. forum. I'll run it by David too and hopefully he's free.

[Andrés Goens]

Great, see you tomorrow then @Patrick Kinnear (and hopefully David too)!

[Patrick Kinnear]

Andrés Goens said:

Great, see you tomorrow then Patrick Kinnear (and hopefully David too)!

Yes, see you there!

[Ramon Fernández Mir]

Reminder: we're meeting today! @Andrés Goens @Tobias Grosser @Paul Jackson @Chris Hughes @Siddharth Bhat @Patrick Kinnear , and anyone else who wants to join :-) I will be there at 12:15.

[Chris Hughes]

MF1 is on the second floor for anyone confused.

[Patrick Kinnear]

Thanks for last week's lunch! For anyone interested, our course pitched at mathematicians starts tomorrow, in Bayes 1.35, 12:00 - 13:30.

Some people expressed an interest in joining, you are most welcome. The course webpage is here.

https://www.maths.ed.ac.uk/~pkinnear/leancourse/

It will be possible to drop in on Zoom too:
https://ed-ac-uk.zoom.us/j/87152560694
Meeting ID: 871 5256 0694
Passcode: LEAN2023

Lastly, we have a private stream here on Zulip for the course. My understanding is I have to add subscribers myself. If you'd like to be added and hang out there and see what we're chatting about, then react to this message and I'll add you.

[Ramon Fernández Mir]

Ah, just saw this... Very exciting. I will come next week. I see @Adrián Doña Mateo is also involved! What a great addition to the team! :-)

[Rayhana Amjad]

Hi there! I'm a new PhD student at Edinburgh working in Lean, I was wondering if the Lean lunches are a weekly fixture and if so whether I could come along?

[Andrés Goens]

Hey @Rayhana Amjad , welcome! That's great, we'd love you to come along. We've been doing them bi-weekly for now, the next one would be next Week Thursday 2023-02-02T12:00:00Z Would also be nice to hear what you're working on and with whom :)

[Rayhana Amjad]

That's fantastic, thanks so much! My supervisor is Liam O'Connor, and I'm currently working on formalising QuickLTL, a variant linear temporal logic with some added operators.

[An Qi Zhang]

I'm guessing the room isn't 1.35 this week?

[Andrés Goens]

no, it's 2.55 today

[An Qi Zhang]

Does anyone know where I could find the files for demo in the course?

[Andrés Goens]

There's a stream for that. We can ask @Patrick Kinnear to add you to it.

[Patrick Kinnear]

Ah sorry @An Qi Zhang , I announced the room change etc on the Zulip stream. Have added you now, thanks for joining us online today :)

[Ramon Fernández Mir]

Hi all! Reminder that we're meeting again today at 12 in MF1 if you're around. :fork_and_knife: :food: @Andrés Goens @Tobias Grosser @Siddharth Bhat @Chris Hughes @An Qi Zhang @Rayhana Amjad @Ke Shen @Patrick Kinnear @Liam O'Connor @Fehr Mathieu @Orestis Melkonian (I hope I'm not missing anyone... :blush:)

[Kevin Buzzard]

You've got quite a crowd up there! That's really great to see.

[Ramon Fernández Mir]

Hello again! I was going to suggest another Lean lunch next week :grinning_face_with_smiling_eyes: I thought it would be a good idea to make a poll to find the best day of the week and time as Thursday at 12 was chosen at random and might not be the best for everyone. Here's the link: https://www.when2meet.com/?18908709-qRbAc I also want to start a mailing list for these meet-ups (and perhaps some other Lean events in the future) so that I don't have to tag everyone here, so let me know if you want to be added. Tagging you all this time though so that you get a notification :sweat_smile: @Andrés Goens @Tobias Grosser @Siddharth Bhat @Paul Jackson @Chris Hughes @An Qi Zhang @Rayhana Amjad @Ke Shen @Liam O'Connor @Patrick Kinnear @Adrián Doña Mateo @Fehr Mathieu @Orestis Melkonian

[Patrick Kinnear]

I'll be travelling, but have a good lunch!

[Andrés Goens]

@Patrick Kinnear If you'd like to join in the future, you're welcome to vote for a day/time that works for you, even if you can't make it next week!

[Siddharth Bhat]

Hello everyone! We have Ashvni Narayanan from Imperial College, who will be visiting Tobias Grosser's lab this week on Thu/Fri. She will be giving a talk on the formalization of p-adic L functions in Lean3, and will be around to chat later.

The talk will be at Informatics forum, IF 1.15, 2PM to 3PM . Do attend, the talk promises to be super interesting!

---

Title : Formalizing p-adic L- functions in Lean 3
Abstract: The Kubota-Leopoldt p-adic L-function is a fundamental number theoretic object. Its characterizing property is its relation to Bernoulli numbers at negative integers. We discuss its formalization in an automated theorem prover, Lean.

Location: Informatics Forum, IF 1.15

---

Click here to add to your calendar!

[Patrick Kinnear]

Hi everyone, we are starting to work on some projects together in the maths course I'm organising. We likely won't finish these by the end of the course but are thinking of organising a hackathon to make progress. If you'd like to be involved or have any ideas you'd like to work on in a hackathon setting, let me know or feel free to join us in our meetings this week and next :)

[Patrick Kinnear]

Hello! The hackathon event associated to our Lean course is planned to take place in two sessions on 25/04 and 11/05. We will be formalising some sections of some mathematical texts in Lean. Please let me know if you'd like to be involved, or if you just want to drop by and say hi :)

[Peiran Wu]

Hello from St Andrews! I just discovered this thread but is the lunch still running over the summer? Not exactly local but I’d love to go and say hi at some point!

[Andrés Goens]

Hey @Peiran Wu! We haven't been running the lunch over the summer, but you coming over to say hi would be the perfect excuse to give it another go!

[Peiran Wu]

Andrés Goens said:

Hey Peiran Wu! We haven't been running the lunch over the summer, but you coming over to say hi would be the perfect excuse to give it another go!

Ah I see. Were you planning to restart this in the new semester? I'll look out for announcements and it should be easy for me to pick a week and join you.

[Tariq Erwa]

Hi everyone, I recently relocated to Glasgow, I am trying to rebuild my social network and meet people with my same interests, when is the next lunch?

[Anton Lorenzen]

Hi Tariq! TypeSig is organising weekly Lean meetups in Edinburgh (mostly for undergrads but PhDs welcome). There is a meeting this evening with talks by myself and John Baez.

[Kevin Buzzard]

Is this unrelated to the lean meeting I went to in Edinburgh last Thursday evening?

[Anton Lorenzen]

It's the same one! Next time, Phil Wadler will talk about the lambda calculus in Lean

[Kevin Buzzard]

I only asked because you said this evening, and it wasn't Thursday :-)

[Monica Omar]

Tariq Erwa said:

Hi everyone, I recently relocated to Glasgow, I am trying to rebuild my social network and meet people with my same interests, when is the next lunch?

Ayo! I'm in Glasgow too!

[Monica Omar]

So, we're running a Lean course for PhDs in Glasgow/Edinburgh this year again, and I was thinking of holding sporadic seminars in formalising mathematics (ssfm), to encourage the students to formalise and all.

Then I thought of maybe making the sporadic seminars in formalising mathematics (ssfm) a separate thing to the course. But, also, mostly encourage the students from the course to give talks.

@Patrick Kinnear then pointed out to me some "Lean lunch" y'all got up in Edinburgh, and thought you guys might be a good target audience for the ssfm.

Let me know what you all think of this.

[Kim Morrison]

I'm in Edinburgh this week; anything Lean related going on?

[Yaël Dillies]

Actually yes! https://www.icms.org.uk/Formalisation Oh I was surprised you didn't know about it. Turns out you're talking there :grinning:

[Eric Wieser]

Kim Morrison said:

I'm in Edinburgh this week; anything Lean related going on?

Well, there's a lot of rain here, and I hear from Joachim that makes Lean things happen!

[Eric Wieser]

(I'm here for the weekend but gone tomorrow morning)

[Kim Morrison]

Oh! Interested in dinner or a drink this evening? There are a number of Lean people presumably arriving this evening.

[Eric Wieser]

I'm entangled with a group of marathon-runners for a very late lunch so am not sure about dinner, but could certainly join for a drink

[Eric Wieser]

(I did not run)

[Rebecca Bellovin]

Is there a stream channel for https://www.icms.org.uk/Formalisation attendees?

[Kevin Buzzard]

If there isn't, there definitely should be!

[Kim Morrison]

It's just been created, I think, and @María Inés de Frutos Fernández will add people!

[María Inés de Frutos Fernández]

I am adding participants now, but we will also advertise it tomorrow on the workshop for those without a Zulip account.

[Anton Lorenzen]

I am based in Edinburgh and would love to meet up! I am a PhD student in programming languages research here, working on improving the reference counting scheme underlying Lean

[Kim Morrison]

(I've sent a DM, suggesting joining some dinner plans this week!)

[Shing Tak Lam]

Hi! I'll be starting my PhD at Glasgow in October in complex differential geometry, (sort of) part of the new AGQ CDT. I did some stuff in Lean in 2019-21, and I would be interested in doing more Lean related stuff when I get to Glasgow.

[Artie Khovanov]

Oh, I don't think I said. I'm starting a PhD at Edinburgh Uni this September, working on AI for maths!

[Alex Brodbelt]

Artie Khovanov said:

Oh, I don't think I said. I'm starting a PhD at Edinburgh Uni this September, working on AI for maths!

Cool! Who are you working with?

Me and some other students will be running a Lean club (with pizza :yum: ) from next wednesday onwards. The first club meeting I will be giving an intro talk to Lean and theorem proving for first years and people wondering what this Lean stuff is - I'm by no means an expert but someone has to spread the gospel. The Lean club is being run by the maths society and typesig, a special interest group of the computer science society.
It would be great to meet you, whether it be at the club or elsewhere :)

[Artie Khovanov]

Alex Brodbelt said:

Artie Khovanov said:

Oh, I don't think I said. I'm starting a PhD at Edinburgh Uni this September, working on AI for maths!

Cool! Who are you working with?

Me and some other students will be running a Lean club (with pizza :yum: ) from next wednesday onwards. The first club meeting I will be giving an intro talk to Lean and theorem proving for first years and people wondering what this Lean stuff is - I'm by no means an expert but someone has to spread the gospel. The Lean club is being run by the maths society and typesig, a special interest group of the computer science society.
It would be great to meet you, whether it be at the club or elsewhere :)

Hi Alex!

I'm working with @Wenda Li.

I've gone to a bunch of TypeSIG stuff already and am looking forward to the Lean workshops -- you're the first one to tell me when they are actually happening lol. Are you with CompSoc, or are you on the maths side?

[Alex Brodbelt]

Artie Khovanov said:

Alex Brodbelt said:

Artie Khovanov said:

Oh, I don't think I said. I'm starting a PhD at Edinburgh Uni this September, working on AI for maths!

Cool! Who are you working with?

Me and some other students will be running a Lean club (with pizza :yum: ) from next Tuesday onwards. The first club meeting I will be giving an intro talk to Lean and theorem proving for first years and people wondering what this Lean stuff is - I'm by no means an expert but someone has to spread the gospel. The Lean club is being run by the maths society and typesig, a special interest group of the computer science society.
It would be great to meet you, whether it be at the club or elsewhere :)

Hi Alex!

I'm working with Wenda Li.

I've gone to a bunch of TypeSIG stuff already and am looking forward to the Lean workshops -- you're the first one to tell me when they are actually happening lol. Are you with CompSoc, or are you on the maths side?

Oh cool, I think someone mentioned a PhD student went to the pub social!

An announcement will be made soon in the server hehe, was just figuring out details of when/where and pizza :pizza: - I am on the committee for Typesig (so yes CompSoc, was in the MathSoc committe last year) as I intend to organise the Lean Club throughout the year.

[Artie Khovanov]

@Alex Brodbelt nice, they said only good things I'm sure ;)
will happily eat the pizza and help some students with their Lean!
also a good opportunity for me to set aside time to work on my personal Lean projects

[Chris Birkbeck]

Hello! I'm in Edinburgh from today until Thursday lunch time. I'm going to be hanging out at the Informatics forum if anyone wants to chat/meet up. I'm also giving a talk there on Wednesday at 4pm in G.03 on formalising the regular case of FLT.

[Alexander Hicks]

I'd expect many people to be around Heriot Watt for the AI & theorem proving workshop going on there on Tuesday. (You might also be in town for this of course.)

[Alex Brodbelt]

Hi! if you want to meet up tomorrow, I am happy to meet up and chat, can even suggest places to visit if you want recommendations :-)

I was also hoping to go to the Heriot Watt AI & theorem proving workshop.

[Chris Birkbeck]

Yeah great! as I say I'll be hanging around the informatics forum near the free desks on the second floor.

[Alex Brodbelt]

Sorry, I meant to send my message yesterday but I got distracted! I can stop by the informatics forum if you would like to meet up today. Otherwise, I can do tomorrow as well :-)

[Chris Birkbeck]

Tomorrow probably works best :)

[Alex Brodbelt]

When does your train leave @Chris Birkbeck ?

[Chris Birkbeck]

Sorry I was gonna message, turns out my train is at 11 so don't think I'll have a chance to stop by the uni!

[Chris Birkbeck]

(I thought it was at 1 but didn't realise the lumo trains a weird)

[Alex Brodbelt]

no worries! safe travels :-)

[Wenda Li]

Safe travel, Chris! :-)