Zulip Chat Archive
Stream: Geographic locality
Topic: Cambridge, UK
Jalex Stark (Feb 28 2020 at 03:43):
There is a regular group meeting here! and an associated private stream on this server! I'm not sure who you ask to be invited
Edward Ayers (Feb 28 2020 at 11:04):
Hi! You can ask me or @Bhavik Mehta to join the secret cambridge stream we meet every Wednesday 15:00 to around 19:00 in MR21 (subject to change) in the CMS
Edward Ayers (Mar 04 2020 at 08:43):
We are in MR10 today, in case someone isn't subscribed to the cambridge stream.
Bhavik Mehta (Nov 12 2020 at 17:31):
Reminder to all in Cambridge that this stream exists
Edward Ayers (Nov 25 2020 at 14:06):
Hi we are having a Cambridge Lean User Group 'CLUG' meetup on Kevin's discord server on the 'live-lean-coding' channel at 15:00. Should be a real slice.
Edward Ayers (Nov 25 2020 at 14:07):
Feel free to drop in even if you don't like Cambridge
Yaël Dillies (Jun 11 2021 at 13:46):
Should we organise meetings in the CMS again now that (first year) exams are finished?
Albert Jiang (Sep 03 2021 at 22:02):
Hi! I'll be starting a PhD at Cambridge in October. Is anyone interested in a HoTT/reasoning/LEAN reading group?
Yaël Dillies (Sep 04 2021 at 07:40):
Yes! We have the CLUG (Cambridge Lean User Group) meeting every Wednesday on Discord and hopefully soon back in person.
Albert Jiang (Sep 04 2021 at 10:31):
That's awesome! I wonder if you could send the Discord link?
Thank you Yaël!
Kevin Buzzard (Sep 04 2021 at 11:09):
Will you be doing mathematics or computer science?
Albert Jiang (Sep 04 2021 at 13:14):
I'll be doing computer science.
Bhavik Mehta (Sep 06 2021 at 17:18):
Albert Jiang said:
Hi! I'll be starting a PhD at Cambridge in October. Is anyone interested in a HoTT/reasoning/LEAN reading group?
You'll probably want to be aware of the existing CL research groups and the alexandria isabelle group as well, if you aren't already
Albert Jiang (Sep 06 2021 at 20:47):
Bhavik Mehta said:
Albert Jiang said:
Hi! I'll be starting a PhD at Cambridge in October. Is anyone interested in a HoTT/reasoning/LEAN reading group?
You'll probably want to be aware of the existing CL research groups and the alexandria isabelle group as well, if you aren't already
Thanks!!!
Eric Rodriguez (Sep 07 2021 at 16:44):
I'm in Cambridge for today and the early parts of tomorrow - would be nice to meet some of you if you're around!
Eric Wieser (Sep 07 2021 at 17:10):
How early are the early parts?
Eric Rodriguez (Sep 07 2021 at 18:17):
Should be around till lunchtime or so :)
Eric Wieser (Sep 08 2021 at 11:29):
I got pulled into a virtual conference, sounds like I probably missed you
Eric Rodriguez (Sep 08 2021 at 13:30):
Sadly so :( will let you all know if I'm up again!
Ferenc Huszár (Sep 16 2021 at 12:13):
Hi everyone - I'm a Senior Lecturer at the Computer Lab working on machine learning. I have absolutely 0 expertise in LEAN or modern theorem proving in general but I started looking into this recently and I'm intrigued.
Jason Rute (Sep 26 2021 at 20:07):
@Ferenc Huszár Welcome! If you haven't already seen it, you should look at the streams #Machine Learning for Theorem Proving and #lean-gptf .
Bhavik Mehta (Oct 20 2021 at 09:28):
The Cambridge Lean user group is back in person! We'll be meeting in MR11 (Pav B) in the CMS at 3pm to 6pm today (and every weds this term). Message me if you need to be let in or need help finding us!
Yaël Dillies (Oct 20 2021 at 11:54):
And this first meeting will be the opportunity to announce a recent result!
Sebastian Reichelt (Oct 24 2021 at 17:50):
Sorry, wrong topic.
Jad Ghalayini (Dec 01 2021 at 20:39):
Bhavik Mehta said:
The Cambridge Lean user group is back in person! We'll be meeting in MR11 (Pav B) in the CMS at 3pm to 6pm today (and every weds this term). Message me if you need to be let in or need help finding us!
Is this still going on over the holidays, and/or next week? Just started a new project using Lean for the first time haha
Shing Tak Lam (Dec 01 2021 at 21:12):
Jad Ghalayini said:
Bhavik Mehta said:
The Cambridge Lean user group is back in person! We'll be meeting in MR11 (Pav B) in the CMS at 3pm to 6pm today (and every weds this term). Message me if you need to be let in or need help finding us!
Is this still going on over the holidays, and/or next week? Just started a new project using Lean for the first time haha
Today will probably be the last in person one for Michaelmas, so I think the plan would be to move online (probably on the Xena server) until Lent term. On the other hand, I (and maybe a few others) will be around in Cambridge over the Christmas vacation.
Joachim Breitner (Apr 20 2022 at 09:13):
I’m traveling to Cambridge for (non-lean) work next week, and wouldn’t mind meeting up likeminded people for dinner or lunch or so. Anyone around?
Yaël Dillies (Apr 20 2022 at 09:14):
Yes, next time is this afternoon on Discord and next Wednesday we will be meeting in person again!
Joachim Breitner (Apr 20 2022 at 09:20):
Cool, can I hang out with you next Wednesday then (April 27)?
Jad Ghalayini (May 12 2022 at 01:33):
@Edward Ayers @Jalex Stark could I by any chance join the aforementioned secret Cambridge stream? Also are meetings going on? Would like to attend next week if so.
Rémi Bottinelli (Sep 11 2022 at 08:46):
Hey! I'll be in Cambridge starting some time next week if all goes well. Would be happy to meet people there!
Joanna Choules (Sep 23 2022 at 12:59):
I didn't get around to this before but I should say that I am another Cambridge-based person, though alas my work hours largely overlap with the meetup times.
Angeliki Koutsoukou Argyraki (Sep 28 2022 at 16:10):
Dear Cambridge Lean users, there is a suggestion to start an informal common seminar series on formalisation of mathematics between the Mathematics Dpt and the Computer Science Dpt, mainly for students. Would you be interested in participating, attending and giving talks? Most of us at the Computer Science Dpt where I'm based work with Isabelle, but the seminar will be open to all proof assistants.
Angeliki Koutsoukou Argyraki (Oct 05 2022 at 17:47):
Who would like to volunteer to give a talk? :) Feel free to write your suggestions below. (Please note that the first couple of meetings at least will be virtual.)
Yaël Dillies (Oct 12 2022 at 14:03):
@Sky Wilshaw and I could give a talk on Con(NF)
Yaël Dillies (Oct 12 2022 at 14:04):
Everyone who is in Cambridge, we're now in MR20 in the CMS until 18:00!
Angeliki Koutsoukou Argyraki (Oct 17 2022 at 21:35):
Angeliki Koutsoukou Argyraki said:
Dear Cambridge Lean users, there is a suggestion to start an informal common seminar series on formalisation of mathematics between the Mathematics Dpt and the Computer Science Dpt, mainly for students. Would you be interested in participating, attending and giving talks? Most of us at the Computer Science Dpt where I'm based work with Isabelle, but the seminar will be open to all proof assistants.
Hi Cambridge Lean Users: the suggested time for the new joint seminar series between the Maths and Computer Science Dpts is every Thursday 16:00-17:00 at the Maths Dpt (though we might have the first session virtually). Can you please give me some feedback if this time is convenient for most people?
Kevin Buzzard (Oct 17 2022 at 21:56):
That's the time that London Learning Lean runs (but obviously you're not in London so this might not be too serious an objection)
Angeliki Koutsoukou Argyraki (Oct 17 2022 at 23:38):
Thank you for letting me know! I was actually hoping that London people may want to come by from time to time- was going to let you know about this. Do you hold your London meeting virtually or in person?
Kevin Buzzard (Oct 18 2022 at 06:00):
They're hybrid
Angeliki Koutsoukou Argyraki (Oct 18 2022 at 11:12):
Thank you @Kevin Buzzard , good to know -does the London meeting finish at 17:00? In that case let me suggest Thursday 17:00-18:00 so that people will be able to attend both if done virtually.
Kevin Buzzard (Oct 18 2022 at 13:01):
Yes it's 4-5.
Rémi Bottinelli (Oct 19 2022 at 13:08):
Angeliki Koutsoukou Argyraki said:
Angeliki Koutsoukou Argyraki said:
Dear Cambridge Lean users, there is a suggestion to start an informal common seminar series on formalisation of mathematics between the Mathematics Dpt and the Computer Science Dpt, mainly for students. Would you be interested in participating, attending and giving talks? Most of us at the Computer Science Dpt where I'm based work with Isabelle, but the seminar will be open to all proof assistants.
Hi Cambridge Lean Users: the suggested time for the new joint seminar series between the Maths and Computer Science Dpts is every Thursday 16:00-17:00 at the Maths Dpt (though we might have the first session virtually). Can you please give me some feedback if this time is convenient for most people?
Hey, is it happening tomorrow? Has a room been chosen yet? Thanks!
Edit. Oh, I guess it's MR20 in the CMS ?
Angeliki Koutsoukou Argyraki (Oct 19 2022 at 14:13):
It's not happening tomorrow, but it's starting next week. I will update here ASAP.
Angeliki Koutsoukou Argyraki (Oct 19 2022 at 14:22):
Meanwhile, will people please respond if the 17:00-18:00 slot works (for those who attend the London meeting virtually)
Angeliki Koutsoukou Argyraki (Oct 20 2022 at 19:06):
UPDATE: The joint seminar on formalisation of mathematics between the Mathematics Dpt and the Computer Science Dpt WILL START IN LENT TERM. Meanwhile, if you like, please feel free to send me talk suggestions.
Yaël Dillies (Oct 23 2022 at 09:09):
Cambridge folks, we have MR19 (in the CMS) booked from 3-6 pm on wednesdays for the rest of term. Please come say hi!
Chris Birkbeck (Oct 30 2022 at 14:22):
I'm giving a talk in the Cambridge number theory seminar (https://talks.cam.ac.uk/show/index/11664) on Tuesday about modular forms and Lean, if anyone is interested. It would be nice to meet some more Lean people :) (Sorry about the shameless self promotion!)
Yaël Dillies (Oct 30 2022 at 14:39):
I should be free!
Kevin Buzzard (Oct 30 2022 at 17:00):
lol the title looks like you're going to prove the modularity conjecture in Lean :-)
Kevin Buzzard (Oct 30 2022 at 17:00):
Maybe you say that's work in progress...
Michael Stoll (Oct 30 2022 at 18:12):
The link for the registration on the Number Theory Seminar page does not seem to work.
Chris Birkbeck (Oct 31 2022 at 09:21):
Kevin Buzzard said:
lol the title looks like you're going to prove the modularity conjecture in Lean :-)
Ha! I forgot to say "statement of"
Chris Birkbeck (Oct 31 2022 at 09:22):
Michael Stoll said:
The link for the registration on the Number Theory Seminar page does not seem to work.
Hmm I'll let them know
Angeliki Koutsoukou Argyraki (Oct 31 2022 at 16:48):
Chris Birkbeck said:
I'm giving a talk in the Cambridge number theory seminar (https://talks.cam.ac.uk/show/index/11664) on Tuesday about modular forms and Lean, if anyone is interested. It would be nice to meet some more Lean people :) (Sorry about the shameless self promotion!)
I am so sorry to miss this, unfortunately I'm not in Cambridge at the moment. I hope we can meet next time you are around! (I'm doing Isabelle though)
Angeliki Koutsoukou Argyraki (Dec 19 2022 at 20:37):
Hi everyone, a reminder that the joint (Computer Science +Mathematics Dpts in Cambridge) seminar series on formalisation of mathematics with interactive theorem provers is starting in Lent! Hope to see many of you :-) Here's the current schedule: http://www.talks.cam.ac.uk/show/index/164015 If you'd like to speak let me know! (2 slots only left in Lent, plus a few future slots in the Easter term)
Angeliki Koutsoukou Argyraki (Jan 14 2023 at 16:54):
Hi everyone, the Cambridge joint seminar is starting this Thursday! :tada:
"Formalisation of mathematics with interactive theorem provers"
(Thursdays at 17:00-18:00, starting this Thursday Jan. 19th.) hosted at the Centre for Mathematical Sciences. (Most meetings will be in person only, but whenever the speaker is remote, it will be possible to participate virtually too).
This is a joint seminar series between the Department of Computer Science and Technology and the Faculty of Mathematics, on the fast-growing area of formalisation of mathematics with proof assistants (interactive theorem provers) such as Isabelle and Lean. All levels welcome. Undergraduate students are particularly encouraged to actively participate.
Our first speaker opening the series is Professor Lawrence C. Paulson: "Formalised Mathematics: Obstacles and Achievements".
You can find the schedule and relevant information at the link below :
http://www.talks.cam.ac.uk/show/index/164015
Please feel free to invite any colleagues who may be interested.
Hope to see many of you!
Angeliki Koutsoukou Argyraki (Jan 18 2023 at 18:18):
Hope to see many of you at the seminar tomorrow!
Angeliki Koutsoukou Argyraki (Feb 01 2023 at 14:20):
Kevin Buzzard will be speaking in person at the formalisation seminar tomorrow! http://www.talks.cam.ac.uk/talk/index/192551
Angeliki Koutsoukou Argyraki (May 04 2023 at 16:12):
@Heather Macbeth Heather Macbeth's talk is starting in a couple of minutes https://talks.cam.ac.uk/talk/index/196702 we are in MR12 and hybrid!
Yaël Dillies (May 04 2023 at 16:15):
I can't seem to join the Zoom meeting! Can you confirm the meeting ID is 379 992 884 209?
Eric Wieser (May 04 2023 at 16:15):
It's a teams meeting!
Eric Wieser (May 04 2023 at 16:15):
It won't work if you use zoom
Yaël Dillies (May 04 2023 at 16:15):
To each their :face_palm:
Mauricio Collares (May 04 2023 at 18:44):
Angeliki Koutsoukou Argyraki said:
Heather Macbeth Heather Macbeth's talk is starting in a couple of minutes https://talks.cam.ac.uk/talk/index/196702 we are in MR12 and hybrid!
Was it recorded? I missed it but the abstract sounds really interesting.
Angeliki Koutsoukou Argyraki (May 05 2023 at 11:25):
It was a really great talk --unfortunately I don't have a recording, sorry. More talks coming up from this Thursday on:
https://talks.cam.ac.uk/show/index/164015
Angeliki Koutsoukou Argyraki (May 09 2023 at 14:43):
This Thursday at the Cambridge joint formalisation seminar we have a hybrid talk (meeting in room MR12 and also online) by Matthieu Piquerez, it's a Coq talk this time! Everyone welcome
https://talks.cam.ac.uk/talk/index/196738
Yaël Dillies (May 09 2023 at 14:56):
Oh nice! We did olympic maths together.
Scott Morrison (May 09 2023 at 22:48):
Zulip's timezone feature is great for seminar announcements: diagram chasing is on at !
Edit: I guess the real point of my message was to request that people announcing time sensitive things use <time, because I am incapable of doing so (correctly) myself...
Eric Wieser (May 09 2023 at 22:50):
No it's not? It's at !
Henrik Böving (May 09 2023 at 22:50):
Luckily we have a uniform way of keeping times!
Angeliki Koutsoukou Argyraki (May 15 2023 at 15:11):
Another cool hybrid talk (MR12 & online) coming up this Thursday: "Explaining Mathematics Using Formalized Mathematics" by Patrick Massot https://talks.cam.ac.uk/talk/index/196750
Angeliki Koutsoukou Argyraki (May 21 2023 at 17:12):
This Thursday Larry Paulson will be speaking at the formalisation seminar in person https://talks.cam.ac.uk/talk/index/196744
Angeliki Koutsoukou Argyraki (May 21 2023 at 18:56):
Everyonee welcome
Angeliki Koutsoukou Argyraki (May 29 2023 at 22:34):
This Thursday at the joint formalisation seminar we are excited to (virtually) welcome @Bjørn Kjos-Hanssen who will present his talk on Lean "The leanest automata"
https://talks.cam.ac.uk/talk/index/196747
Everyone welcome
Angeliki Koutsoukou Argyraki (Jun 02 2023 at 17:10):
Next Thursday at the Cambridge joint formalisation seminar
@Alex J. Best will be visiting us from London to present his talk https://talks.cam.ac.uk/talk/index/196741
Everyone welcome! (in person only)
Angeliki Koutsoukou Argyraki (Jun 12 2023 at 13:37):
This Thursday we are very happy to welcome @Sebastien Gouezel for a hybrid talk https://talks.cam.ac.uk/show/index/164015
Everyone welcome!
Chris Hughes (Jun 15 2023 at 12:46):
I'll be at the talk in Cambridge today
Angeliki Koutsoukou Argyraki (Jun 17 2023 at 17:59):
Next Thursday we'll have another exciting talk at the seminar, this time by @Yaël Dillies (in person):
"Roth numbers: Upper, lower bounds, and related constructions"
https://talks.cam.ac.uk/talk/index/202663
Everyone welcome
Angeliki Koutsoukou Argyraki (Jul 04 2023 at 11:54):
Hi, most of you probably already know that CICM will take place in Cambridge this September! I just want to let you know about these two EuroProofNet workshops that I am co-organising that will take place at the Cambridge Computer Science Dpt around the same time. I believe local people who already live in Cambridge cannot apply for funding, but you may want to attend some of the talks and/or submit a talk proposal
Angeliki Koutsoukou Argyraki (Sep 03 2023 at 22:33):
This is just a reminder about the two EuroProofNet workshops that are taking place this week at the Computer Laboratory: https://europroofnet.github.io/cambridge-2023/ Everyone interested is most welcome to attend/no registration needed!
Tobias Grosser (Sep 14 2023 at 17:50):
Dear team Cambridge. I will be in Cambridge next week Mon-Wed. In case someone is interested to catch a coffee at the computer lab, let me know.
Anand Rao Tadipatri (Jan 10 2024 at 17:00):
The Cambridge talk series on the formalisation of mathematics with interactive theorem provers will be resuming in the Lent term of 2024 (with @Jonas Bayer, @Angeliki Koutsoukou Argyraki and @Anand Rao Tadipatri as the organisers). This is a joint seminar series between the Department of Computer Science and the Faculty of Mathematics on the formalisation of mathematics with interactive theorem provers (proof assistants) and related topics. The talks will be from 5 PM to 6 PM on Thursdays in room MR-14 of the Centre for Mathematical Sciences (livestreamed whenever the speaker is remote).
The details of the talks are available on this webpage, which will be regularly updated throughout the term: https://talks.cam.ac.uk/show/index/164015.
Anand Rao Tadipatri (Jan 10 2024 at 17:00):
Our first talk by @Siddhartha Gadgil (Indian Institute of Science) on the topic "Towards Autoformalization and Mathematical Reasoning using language models" will be on the 17th of January (Wednesday) between -. The details of the talk are available at https://talks.cam.ac.uk/talk/index/210154. Please note that this is scheduled at a different time than the rest of the talks in the series.
Kim Morrison (Jan 10 2024 at 22:52):
It's very helpful if announcements can use the <time command, which pops up a time picker, then displays times in users' local timezones!
Eric Wieser (Jan 10 2024 at 23:44):
I believe that's -
Anand Rao Tadipatri (Jan 17 2024 at 11:46):
This is a reminder for the first talk which will be starting in close to an hour. It will be also be live-streamed at
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Eric Wieser (Jan 17 2024 at 13:30):
Is the any hope of switching to Zoom for future streams? It took me 10 minutes to finally have teams behave well enough to connect to the talk, and it seems the teams installation in the room took almost half an hour.
Kevin Buzzard (Jan 17 2024 at 13:42):
I asked Anand about this when I saw them on Monday at CPP and they said that Cambridge doesn't have a Zoom license so if it's a Zoom talk then it can only be 45 minutes ;-)
Anand Rao Tadipatri (Jan 17 2024 at 14:27):
We're sorry for the technical difficulties with the recordings, the talk was also recorded through the cameras in the room and will be available via Moodle. We will also look into switching to Zoom for the future talks.
Anand Rao Tadipatri (Feb 07 2024 at 09:23):
This is a reminder for this week's talk by @Kevin Buzzard titled How to Prove Fermat's Last Theorem. Further details about the talk are available at https://talks.cam.ac.uk/talk/index/210157.
The talk will be live-streamed in MR-14 at , and can also be followed at this link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Anand Rao Tadipatri (Feb 07 2024 at 09:23):
The talks from this series may be uploaded online soon with the permission of the speakers.
Anand Rao Tadipatri (Feb 08 2024 at 17:12):
This is a reminder for the talk which is being livestreamed now.
Oisin McGuinness (Feb 09 2024 at 16:19):
Anand Rao Tadipatri said:
This is a reminder for the talk which is being livestreamed now.
Hi, is a recording of this talk of @Kevin Buzzard available or going to be available?
Thanks!
Kevin Buzzard (Feb 09 2024 at 16:27):
It was a standard Kevin waffle talk, don't get too excited. My audience was first year undergrad mathematicians and professors of computer science so it wasn't some technical explanation of what the FLT proof looks like 30 years post-Wiles, it was much more a "general audience" talk. I guess @Anand Rao Tadipatri is the person to talk to about the details of possible uploading.
Oisin McGuinness (Feb 09 2024 at 17:03):
Thanks for the reply. I enjoy 'waffle' sometimes... The key part of interest is understanding more of your top level strategy for the project, but that will emerge in due course I expect.
Kevin Buzzard (Feb 09 2024 at 17:08):
Yeah, by far the most interesting mathematical question people want to know the answer to is "how are you going to avoid Ribet and Langlands--Tunnell", to which the answer is "Taylor and I have a document which explains this but it's not public and when term is done I'm going to spend a lot of time turning it into a blueprint, so ask again in late April".
Anand Rao Tadipatri (Feb 11 2024 at 20:28):
Hi, we plan to put up recordings of the talks up on the webpage soon (with the permission of the speakers). I'll share the relevant links here when that's done.
Anand Rao Tadipatri (Feb 14 2024 at 15:56):
This is a reminder for this week's talk by @Jeremy Avigad titled Structures in dependent type theory. Further details about the talk are available at https://talks.cam.ac.uk/talk/index/210391.
The talk will be live-streamed in MR-14 at , and can also be followed at this link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Anand Rao Tadipatri (Feb 21 2024 at 17:25):
Our next talk is by @Artem Khovanov, @Wenda Li and Michael Nedzelsky on Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry. Further details can be found here: https://talks.cam.ac.uk/talk/index/211648.
The talk will be live-streamed in MR-14 at , and also on the usual link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Geoffrey Irving (Feb 28 2024 at 16:49):
I'll be in Cambridge tomorrow to give a Mandelbrot set talk if anyone wants to meet up. The following image is sadly not formalized (much faster to prepare a talk using Python + Jax + GPUs, alas):
Anand Rao Tadipatri (Mar 07 2024 at 09:43):
Our next talk is by @Lawrence Paulson on Formalising (part of) the Diagonal Ramsey Paper. Further details can be found at http://talks.cam.ac.uk/talk/index/210400.
Anand Rao Tadipatri (Mar 14 2024 at 08:18):
Our last talk for this term is by @Adam Topaz on Lawvere theories in Lean. The talk will be live-streamed at on our usual link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Further details can be found here: https://talks.cam.ac.uk/talk/index/212215
Adam Topaz (Mar 14 2024 at 19:42):
In case anyone is interested, here is a copy of the slides from the talk:
pres.pdf
Anand Rao Tadipatri (Apr 24 2024 at 22:13):
The seminar series will be resuming tomorrow. Our first talk for the term is by @Mohammad Abdulaziz on the topic "Formalising Theory of Combinatorial Optimisation". It will be live-streamed tomorrow at on the link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
We also have another talk at by Michael Douglas on the topic "Can a computer judge interestingness?" which will be live-streamed on the same link.
Anand Rao Tadipatri (Apr 28 2024 at 19:47):
This is a reminder for the talk by Michael Douglas at .
Anand Rao Tadipatri (May 01 2024 at 20:41):
Our next talk is by @Johan Commelin on Condensed Type Theory. The talk is at and can be followed on this link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Alexander Hicks (May 08 2024 at 14:20):
Are any of these talks recorded and available online by any chance @Anand Rao Tadipatri ?
Anand Rao Tadipatri (May 08 2024 at 14:23):
Most of these talks have been recorded. We haven't been able to put them up online yet, but plan to do that by late June (but hopefully sooner).
Anand Rao Tadipatri (May 08 2024 at 22:20):
Our next talk is by @Tomas Skrivan on _Scientific Computing in Lean_: https://talks.cam.ac.uk/talk/index/216106. It will be live-streamed as usual at on the link:
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Alexander Hicks (May 09 2024 at 12:51):
Anand Rao Tadipatri said:
Most of these talks have been recorded. We haven't been able to put them up online yet, but plan to do that by late June (but hopefully sooner).
Amazing, thanks!
Anand Rao Tadipatri (May 15 2024 at 13:07):
We have a talk by @Patrick Massot at on teaching using a proof assistant and controlled natural language. The talk will be live-streamed at
Meeting ID: 370 771 279 261
Passcode: iCo7a5
Anand Rao Tadipatri (May 22 2024 at 16:54):
We have a talk by Georges Gonthier at titled Little theories for big formal proofs. We will be live-streaming on the following link: https://cam-ac-uk.zoom.us/j/89458346264?pwd=Wkt2NUNwV0xzTGkyR2hGQUVGRThsUT09.
Further details about the talk can be found on this page: https://talks.cam.ac.uk/talk/index/216109.
Anand Rao Tadipatri (Jun 12 2024 at 16:20):
Our last talk for this term is by Tobias Nipkow at on the topic Alpha-Beta Pruning Explored, Extended and Verified. The talk will be live-streamed via Zoom: https://cam-ac-uk.zoom.us/j/89453157536?pwd=lUNbK9xamhh2B6O7Df6bNfUEEkGrVo.1.
The abstract for the talk is available at https://talks.cam.ac.uk/talk/index/216049.
William Sørensen (Aug 14 2024 at 09:52):
Hi!
I am a student in Cambridge (incidentally also in Caius like Yaël), I was simply wondering are there any groups / socs that align with Lean here?
Yaël Dillies (Aug 14 2024 at 09:55):
There is CLUG which I was running while I was there. Not sure if there are any plans for next year. Else there is the research group around Tim Gowers (ask @Anand Rao Tadipatri or @Jonas Bayer) in the maths department or the one around @Tobias Grosser in the CS one.
William Sørensen (Aug 14 2024 at 09:57):
Oki nice to know, yeah I am currently working under @Alex Keizer (transitively Tobias) on co-recursion / -induction. Hoping to be going to some Lean stuff next year so would be fun it there was stuff for it
Eric Wieser (Aug 14 2024 at 10:05):
Why is Caius so Lean-heavy; is this your doing @Yaël Dillies?
Yaël Dillies (Aug 14 2024 at 10:06):
Certainly I have inspired @Patrick Luo and Kim Worrall, who I believe is a friend of William, but that's probably all I have done!
William Sørensen (Aug 14 2024 at 10:07):
Honestly I have no idea how I ended up getting into Lean, it just seemed fun
William Sørensen (Aug 14 2024 at 10:08):
Also Yaël ive been trying to convince Kim to formalise her topology / higher cat stuff in lean but to no avail so far
William Sørensen (Aug 14 2024 at 10:08):
at this rate we will just get more and more
Yaël Dillies (Aug 14 2024 at 10:10):
William Sørensen said:
Also Yaël ive been trying to convince Kim to formalise her topology / higher cat stuff in lean but to no avail so far
Me too. It's an uphill battle
William Sørensen (Aug 14 2024 at 10:13):
She seems very interested though I dont think theres a lot of convincing left haha.
Plus I want to learn some topology so at least we yap about the little stuff that Buzzard covered in the formalizing maths course of it. Quite fun but I want to find resources to learn more as i think this would also convince her to use lean as well
Anand Rao Tadipatri (Aug 15 2024 at 08:27):
We sometimes have informal talks on topics related to ITP and ATP. We won't have any this month, but if there are any happening next month, I could announce on the CLUG group.
Kevin Buzzard (Aug 20 2024 at 09:02):
If you want more topology in the formalising maths course then tell @Bhavik Mehta who's teaching it next year
William Sørensen (Aug 20 2024 at 11:55):
oh nice. i find its a fun resource as it teaches maths in a way that i quite like as a comp-sci. would honestly like to learn more as theres so much maths i want to explore. and @Siddharth Bhat is repeatedly nerd-sniping me into doing topology.
Would be nice to just have a bank of problems and definitions that can be goofed around with and proved. like i was trying to prove the defn used in the course to show that the metric space defn of continuous and the topological one are related as they are. just cool anyway
Siddharth Bhat (Aug 20 2024 at 14:14):
@William Sørensen if you want a computer sciencey explanation on topology (Not sure @Kevin Buzzard approves :wink: ) I'd suggest reading "frames and locales": https://link.springer.com/book/10.1007/978-3-0348-0154-6. It sets up similar theory, in a way that's accessible to our people, 'cause it takes the computational view on topology!
William Sørensen (Aug 21 2024 at 08:29):
haha nice that sounds like a fun thing to look into. i will definitely take a look and see if i can find this in one of the libraries before i go back to norway. thanks for the recomendation!
Tobias Grosser (Aug 23 2024 at 13:29):
We have a fun workshop here in Cambridge. Not very lean heavy, but some of the attendees use lean. https://app.youform.com/forms/colm20c6 Feel invited to join.
Jakob von Raumer (Sep 06 2024 at 14:38):
I'm in Cambridge until at least the end of the month working with @Tobias Grosser and team, happy to meet Lean people :smile:
Anand Rao Tadipatri (Sep 23 2024 at 15:21):
There are a few of us in the mathematics department, and I think it would be nice to meet if you're still around!
Jakob von Raumer (Sep 24 2024 at 09:18):
Yes, still there until Thursday next week! Happy to meet up anytime :grinning:
Jakob von Raumer (Sep 24 2024 at 09:52):
@Bhavik Mehta are you still in Cambridge?
Bhavik Mehta (Sep 24 2024 at 10:03):
Not any more, unfortunately!
Henrik Böving (Sep 24 2024 at 10:16):
I'm also going to be in Cambridge from to
Anand Rao Tadipatri (Sep 24 2024 at 15:39):
How about at Churchill College?
Jakob von Raumer (Sep 24 2024 at 15:50):
Sounds good!
Anand Rao Tadipatri (Oct 01 2024 at 09:13):
@Jonas Bayer @Jovan Gerbscheid and @Jacob Loader will also be joining for lunch today. We look forward to meeting you, @Jakob von Raumer and @Henrik Böving!
Jakob von Raumer (Oct 01 2024 at 09:39):
Should we just meet at the entrance to the dining hall?
Anand Rao Tadipatri (Oct 01 2024 at 09:51):
That sounds good to me.
Tom (Oct 01 2024 at 17:49):
This sounds fun. Now I'm wishing I had flown back for my reunion, I would have loved the opportunity to join! :smile:
Tomas Skrivan (Oct 04 2024 at 09:55):
I will also be in Cambridge 7-11.10. :smile: @Henrik Böving we should meet before you leave. What about Monday evening or anytime on Tuesday?
Henrik Böving (Oct 04 2024 at 09:56):
Sure!
Angeliki Koutsoukou Argyraki (Oct 08 2024 at 17:27):
The seminar series "Formalisation of mathematics with interactive theorem provers"
hosted at the Cambridge Centre for Mathematical Sciences is resuming. There will be both in-person and online talks, every Thursday at 17:00-18:00 UK time.
The first talk of the term will take place this Thursday 10 October, and it will be by Maximilian Doré (University of Oxford)
on Cubical Type Theory: "Reasoning with Kan fillings about Morse reductions":
https://talks.cam.ac.uk/talk/index/222244
This is a joint seminar series between the Cambridge Department of Computer Science and Technology and the Faculty of Mathematics.
You can find the schedule (in progress) and relevant information at the link below:
https://talks.cam.ac.uk/show/index/164015
Please feel free to invite your students and any colleagues who may be interested.
All levels welcome. Undergraduate students are particularly encouraged to actively participate.
For any questions or talk suggestions, please contact me or my co-organisers Anand Rao Tadipatri @Anand Rao Tadipatri and Jonas Bayer @Jonas Bayer
Pietro Monticone (Oct 08 2024 at 18:16):
Thank you for posting @Angeliki Koutsoukou Argyraki. Will the seminars be recorded and made public?
Jonas Bayer (Oct 08 2024 at 18:41):
Hi @Pietro Monticone ! We plan on recording the seminar talks and uploading them to a Youtube channel if speakers agree. That has been somewhat complicated to set up in the past (since we were using both Teams and Zoom, with two separate organiser accounts etc.) But we hope that this term the process will work more smoothly.
Anand Rao Tadipatri (Oct 22 2024 at 14:32):
We have a talk this Thursday by @Sky Wilshaw on formalizing the consistency of Quine's New Foundations: https://talks.cam.ac.uk/talk/index/222292. We plan to have lunch with the speaker around at Churchill College; anyone interested is welcome to join.
Anand Rao Tadipatri (Nov 14 2024 at 10:06):
We have a talk by @María Inés de Frutos Fernández today at on formalizing the divided power envelope in Lean.
Further details are available at https://talks.cam.ac.uk/talk/index/222778.
The Zoom meeting details are
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
Anand Rao Tadipatri (Dec 04 2024 at 16:51):
Our last talk for this term will be at by @Yaël Dillies on How to teach Fourier analysis to a large library of formalised mathematics: https://talks.cam.ac.uk/talk/index/223858.
The talk will be live-streamed at on
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
We plan to have lunch with the speaker at ; anyone interested is welcome to join.
Yaël Dillies (Dec 04 2024 at 16:55):
After the talk, I will post relevant documentation in #general > Online talk on managing a project depending on Mathlib
Anand Rao Tadipatri (Jan 17 2025 at 08:17):
We'll be resuming the Formalization of Mathematics talk series this term with talks taking place weekly on Thursdays between 5 pm and 6 pm UK time.
The list of talks and speakers for this term is available here: https://talks.cam.ac.uk/show/index/164015. Recordings of some of our previous talks in this series are now available on our YouTube channel (https://www.youtube.com/@FormalisationSeminarCam/videos) and we are in the process of making more talks available shortly.
Our first talk this term is by @Siddharth Bhat at : https://talks.cam.ac.uk/talk/index/224860.
Anand Rao Tadipatri (Jan 23 2025 at 10:12):
This is a reminder for today's talk by @Siddharth Bhat at .
Anand Rao Tadipatri (Jan 23 2025 at 17:00):
Here's the meeting link: https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Anand Rao Tadipatri (Jan 29 2025 at 09:16):
This week's talk is by @Emily Riehl on Prospects for formalizing the theory of weak infinite-dimensional categories.
The talk will be livestreamed at on our usual Zoom link: https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1.
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
Further details, including the abstract, can be found here: https://talks.cam.ac.uk/talk/index/224938.
Emily Riehl (Jan 29 2025 at 22:38):
Btw, I've already posted the slides in case anyone wants a preview. And if you catch any typos, please let me know!
Tobias Grosser (Jan 31 2025 at 07:35):
We are hosting on Feb 12 a compiler social here in Cambridge (https://grosser.science/compiler-social-2025-02-12/). While the social is only tangentially related to Lean, there are likely a number of Lean people around. In particular, we are hosting in the same week some lean folks from Galois and Lindylabs who develop with us a Lean backend for Sail. If this interests you, join us at the social or ping me separately.
Jonas Bayer (Feb 06 2025 at 13:14):
This is a reminder for today's talk by Thomas Ammer at .
Here's the meeting link: https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Anand Rao Tadipatri (Feb 12 2025 at 10:41):
We have a talk tomorrow at by @David Ang on Algebraising foundations of elliptic curves: https://talks.cam.ac.uk/talk/index/225244.
The talk will be delivered in hybrid-mode, livestreamed on our usual Zoom link
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
We will be having lunch with the speaker at at Churchill College; anyone interested is welcome to join.
Ching-Tsun Chou (Feb 12 2025 at 23:57):
Would it be possible to record this talk and put it on YouTube?
Anand Rao Tadipatri (Feb 13 2025 at 10:36):
Yes, that is the plan!
Jakob von Raumer (Feb 13 2025 at 16:53):
CS people will arrive a bit late :grimacing:
Jakob von Raumer (Feb 13 2025 at 17:03):
Which building is it?
Anand Rao Tadipatri (Feb 13 2025 at 19:21):
I'm sorry for not seeing this in time! We're usually in MR-14.
David Ang (Feb 13 2025 at 19:27):
Here are the slides with typos corrected
Anand Rao Tadipatri (Feb 19 2025 at 22:45):
We have an in-person talk by @Jujian Zhang at on Formalising Brauer Group and Group Cohomology in Lean4. The abstract can be found here: https://talks.cam.ac.uk/talk/index/225613. We will be live-streaming on our usual Zoom link https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1.
Anand Rao Tadipatri (Feb 20 2025 at 23:50):
There will be no talks for the next two weeks, we will have one on the 12th of March instead.
Anand Rao Tadipatri (Mar 05 2025 at 22:38):
This is a reminder that there will be no talk tomorrow, but we have two talks coming up next week.
Anand Rao Tadipatri (Mar 11 2025 at 19:48):
We have two talks this week. The first one is at by @Francisco Ferreira titled Why do I write proofs?.
The other is by Tristan Stérin and Maja Kądziołka at on the formal verification of the 5th Busy Beaver value.
Both talks will be live-streamed on our usual Zoom link https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1.
Anand Rao Tadipatri (Mar 19 2025 at 16:59):
Our last talk for this term is by @David Wang tomorrow at on Verified unsolvability of temporal planning: https://talks.cam.ac.uk/talk/index/225322.
The talk will be in-person and livestreamed on our usual Zoom link https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1.
Anand Rao Tadipatri (Apr 29 2025 at 09:47):
We have a talk this week by @Kevin Buzzard at titled Formalizing Fermat: an update.
Further details, including the abstract, are available here: https://talks.cam.ac.uk/talk/index/225178.
The talk will also be livestreamed on our usual Zoom link:
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
Anand Rao Tadipatri (May 01 2025 at 17:04):
I'm sorry, the meeting seems to have timed out abruptly, presumably because it's been exactly an hour. I'll resume the meeting for the online participants in case anyone has any questions.
Oisin McGuinness (May 01 2025 at 17:57):
I was connected via Zoom, enjoyed the talk, and was enjoying the questions.... I understand there is going to be a recording, will it contain the extra part after 'resuming the meeting'?
Thanks!
Last updated: May 02 2025 at 03:31 UTC