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.
Last updated: Dec 20 2023 at 11:08 UTC