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 :-)