Seminar -- London Learning Lean

Stream: maths

[Kevin Buzzard]

I am sufficiently senile that I can't remember whether I mentioned this seminar here yet. London Learning Lean https://researchseminars.org/seminar/LondonLearningLean is a seminar generally on MSc level mathematics in Lean. It's hybrid and in particular you can watch it on Zoom. It's on Thursdays at 4pm UK time for the next 11 weeks, so the first one is at 2022-01-13T16:00:00Z (it's Maria talking about her work on adeles and ideles and their relationship to class groups).

[Johan Commelin]

Can't wait to see a talk about the LLL algorithm in the LLL seminar :grinning:

[Kevin Buzzard]

Are you offering?

[Kevin Buzzard]

I'm absolutely serious -- if there's anyone out there who wants to give a talk then please get in touch; I filled essentially all of this term's slots with a bunch of people around me in London and on the Discord before I even started thinking about the Zulip people. I fully intend to run the seminar next term too.

[Johan Commelin]

Kevin Buzzard said:

Are you offering?

Not yet. I would have to dive into the LLL algorithm again.

[Stuart Presnell]

Just a reminder (as I haven't seen it posted here this week) that this week's talk will be starting in a few minutes: Chris Birkbeck on "Modular forms and Eisenstein series".
https://researchseminars.org/talk/LondonLearningLean/2/

[Stuart Presnell]

At least, I assume it's going ahead — @Kevin Buzzard notes on that page that he's not around this week to run things.

[Stuart Presnell]

(deleted)

[Kevin Buzzard]

London Learning Lean has been running for a few months this year, but I only just found the time to upload the videos to YouTube. Just uploaded are:

Jan 12 Billy Miao: Ostrowski's theorem
Jan 19 Ashvni Narayanan: p-adic measure theory
Jan 26 Oliver Nash: Ergodicity and Gallagher's theorem
Feb 02 Alex Best: Solving Diophantine equations via the class group
Feb 09 Anand Rao Tadipatri + Siddhartha Gadgil: Formalising Giles Gardam's disproof of Kaplansky's Unit Conjecture
Feb 16 Ella Yu + Xiang Li: Euler's Totient Theorem and the Prime Number Theorem
Feb 23 Jineon Baek: On the Erdős-Tuza-Valtr Conjecture
Mar 09 Jujian Zhang: Flat modules
Mar 16 Joy Hu/Runchang Li: Some Basics of Gaussian Measure in Lean
Mar 23 Matej Penciak: Implementing Cryptographic Primitives in Lean 4
May 04 Amelia Livingston: Tori

You can see the videos on the London Learning Lean playlist on the Xena Project Youtube channel.

I'm always looking for people (especially undergraduates, masters or PhD students) who have formalised something they think they can turn into a talk. Probably I'll start the seminar again in October.