Bristol, England

Stream: Geographic locality

[Laura Monk]

Hi! I am just getting started in Lean and based in Bristol. Thought I would pop a message in case anyone is around :).

[Joseph Tooby-Smith]

Hi Laura! I'm moving to Bath next month to start a faculty position, so will be near by! I'm mainly working on #PhysLean , but I'm interested in all things Lean and maths as well.

[Johan Commelin]

Welcome to Zulip!

[Laura Monk]

Joseph Tooby-Smith said:

Hi Laura! I'm moving to Bath next month to start a faculty position, so will be near by! I'm mainly working on #PhysLean , but I'm interested in all things Lean and maths as well.

Nice! I'd be quite curious to hear about #PhysLean, we should meet after the summer.

[Joseph Tooby-Smith]

Yeah definitely! Let's touch base then.

[Adhyayan Sharma]

Hello everyone! I’m a student at UoB and I’m learning Lean this summer. Nice to see we have a channel for Bristol now :smiley:

[Mukesh Tiwari]

Hi @Laura Monk and @Joseph Tooby-Smith I am based in Swansea, not very far from Bristol and Bath. I dabble with Lean occasionally (I am a regular Rocq user and I hope that is not a deal breaker :)).

[Freddie Nash]

I'm regularly in Bristol: definitely keen to hear if anything Lean (or formal verification or constructive mathematics in general) is happening nearby

[Joseph Tooby-Smith]

Hey all - i just got settled in Bath, should we organize a meet up at some point?

[Laura Monk]

Good idea! I am busy travelling until mid-September but have more time after that

[Freddie Nash]

I also happen to be overwise occupied until early/mid-September

[Joseph Tooby-Smith]

Ok, let us aim for sometime late September then.

[Freddie Nash]

I'm back to having nothing on: is there a particular day of the week that works for people? (anything works for me with a bit of notice)

[Wrenna Robson]

Oh hey, I just noticed this. I am in Bristol and a Leaner (Leanoid? Leanist?)

[Freddie Nash]

I'm (probably) moving to Bristol next week, and will be at the university on the weekend on other business if anyone else is around; otherwise, maybe we should try to arrange something before the new year.

[Laura Monk]

Hi! I have had some personal things to deal with this term which have delayed my Lean greatly. I am getting back at it now. Would people like to meet sometime in December?

[Wrenna Robson]

Yes!

[Wrenna Robson]

Are you based at the University of Bristol or UWE?

[Laura Monk]

UoB

[Laura Monk]

/poll Hi! Here are a few dates suggestions for meeting at the Fry Building on Woodland road:
Monday 1/12 at 2pm
Monday 8/12 at 10am
Wednesday 10/12 at 2pm
Friday 12/12 at 10am

[Laura Monk]

This is just a few options, anyone interested in joining, please let us know your constraints

[Wrenna Robson]

I work from home (Newport, Wales) on Mondays and Fridays

[Freddie Nash]

Anytime suits me with a week or so of warning

[Laura Monk]

Hi @Adhyayan Sharma, @Mukesh Tiwari and @Joseph Tooby-Smith, would you like to join?

[Joseph Tooby-Smith]

Added my availability to the list :). Annoyingly my December is pretty full with conferences and travel :(.

[Mukesh Tiwari]

Added my preferences. I cannot do 10th December and 12th December.

[Laura Monk]

I cannot do Thursday afternoon but morning could work

[Ronan Lamy]

Hi! I'm a software developer learning Lean, I'm keen for a local meet-up. I'm probably available any time, but afternoons are easier.

[Adhyayan Sharma]

Added my preferences too! I have my term exams quite close to 8th December so anything earlier would be easier :)

[Adhyayan Sharma]

Apologies if you’re seeing this a second time, Zulip was giving me a weird server error

I have my term exams quite close to 8th December, so any time earlier would work well :)

[Laura Monk]

Hi! thanks everyone for replying, I added an option on Thursday morning as it looks like Thursday afternoon works for everyone but me ;)

[Freddie Nash]

Is the plan then to meet at UoB? Will access for externals be a problem?

[Laura Monk]

I will discuss this with the head of school and let you know.

[Laura Monk]

Looks like Thursday 4/12 at 10am works for everyone except perhaps @Ronan Lamy , would that work for you? We can set the date then :)

[Laura Monk]

I think we'll be able to organise the event here in UoB, I'll keep you updated.

[Ronan Lamy]

Yes, Thursday morning works for me.

[Laura Monk]

Amazing, let's set this date then! I'll send more practical info soon.

[Wrenna Robson]

Brilliant

[Laura Monk]

Hi! Here is a registration link for the meet-up:
https://forms.office.com/Pages/ResponsePage.aspx?id=MH_ksn3NTkql2rGM8aQVG92eI-w7YZtBmluGqMF-NeJUMk5MV0RKWFJWR0NLMFowREJNV1IyTlZNUi4u

[Wrenna Robson]

This is in two days, right?

[Freddie Nash]

That's my understanding

[Laura Monk]

Hi! Just a little reminder about our meeting tomorrow at 10 am in room G.07 of the Fry Building in Bristol! Please register if you wish to attend. See you :)

[Mukesh Tiwari]

Hi all, it seems I will be missing the meeting tomorrow because something else has come up. I hope to see you all at some point in the future, if not tomorrow.

[Joseph Tooby-Smith]

Thank you for putting the effort in to make this happen, and dealing with the logistics @Laura Monk ! Really appreciate it. I'm looking forward to meeting people tomorrow :).

[Laura Monk]

Mukesh Tiwari said:

Hi all, it seems I will be missing the meeting tomorrow because something else has come up. I hope to see you all at some point in the future, if not tomorrow.

Oh that is a shame! There should be others if all goes well :)

[Laura Monk]

I will bring some nibbles but not coffee so if you want some please bring it. And adaptors for your laptops if you wish to show us something!

[Wrenna Robson]

I will be there.

[Freddie Nash]

Heads up: the room is presently locked (not sure if that's a problem, however)

[Ronan Lamy]

On my way, sorry I'm late!

[Laura Monk]

Thank you again for the lovely meeting! I will send date suggestions early January to organise another meeting in January / early Feb.

[Adhyayan Sharma]

Thank you so much for organising this meeting @Laura Monk , looking forward to the next one!

[Wrenna Robson]

Really happy to help out with any aspect of making this happen again.

[Freddie Nash]

My schedule has finally normalised again, so I'd be keen for another Lean meetup in the coming weeks if people have time

[Wrenna Robson]

That would be good.

[Mukesh Tiwari]

If you are willing to travel to Swansea, I can arrange a place for meeting. Moreover, if you want , you can give a talk at our theory group.

[Wrenna Robson]

I live in Newport so...

[Wrenna Robson]

I had heard there was some kind of formalisation group at Swansea!

[Mukesh Tiwari]

Then it should not be a problem. Besides, it is a very nice place :) (Swansea is on par with Melbourne, in my opinion).

[Wrenna Robson]

It's lovely, visited there recently. Would happily move there.

[Mukesh Tiwari]

Yes, we have and I am one of those people but we have a bigger group that works in railway software verification.

[Wrenna Robson]

Cool!

[Laura Monk]

Hi everyone! With a bit for delay, here is a pool for the next Bristol local meeting :)

[Laura Monk]

/poll When would you be available to meet in the Fry Building, Bristol?
Thursday 5/2 at 10am
Thursday 19/2 at 10am
Thursday 26/2 at 10am

[Laura Monk]

I put only Thursdays as I remembered that was pretty much the intersection of our constraints, but please do add extra dates to the pool if none of these fit.

[Wrenna Robson]

Ooh btw I mentioned some of the work that went into this paper (https://eprint.iacr.org/2026/107) last time

[Wrenna Robson]

if it is of interest

[Laura Monk]

Congrats Wrenna!

[Laura Monk]

Ok, I suggest we meet at 10am on Thursday 5/2. I'll book a room, anyone who wants to join please contact me by direct message.

[Adhyayan Sharma]

Apologies, I won’t be able to attend meetings till March due to uni work, but I hope everyone has a great time!

[Laura Monk]

Oh, that is a shame - wish you all the best with the uni work!

[Adhyayan Sharma]

Thank you so much! I’ll definitely be there after I’m done with my dissertation

[Ronan Lamy]

I won't be able to attend, enjoy the meeting!

[Laura Monk]

Oh that is a shame, see you another time Ronan!

[Wrenna Robson]

This message just reminded me it's happening in 15 minutes!

[Laura Monk]

Thank you for the lovely meeting! I think every other month is a good frequency on my end; I will try and start a pool in a month or so.

[Wrenna Robson]

I have become aware of at least one other Lean user at the university and am wondering that we should publicise it more as a thing.

[Wrenna Robson]

Inspired by https://yaeldillies.github.io/slug.html, I am wondering about a "Bristol Lean Users and Enthusiasts" (BLUE) group

[Michael Rothgang]

Comment from the sides: BLUE is a great acronym :-)

[Wrenna Robson]

Yeah I was very pleased with myself for that :D

[Laura Monk]

Happy to advertise more! I can definitely advertise at the level of the School of maths and perhaps print a poster for the students.

[Wrenna Robson]

I think it would certainly be good to know about undergraduates/postgrads who are interested!

[Wrenna Robson]

Perhaps I should whip up a little website for "The BLUE Group".

[Laura Monk]

If you are keen yes please go for it! :)

[Kevin Buzzard]

I think that there were two reasons I was able to attract undergrads to my formalizing club in 2017 (when, let me stress, I knew very little myself about Lean and watched with interest as undergraduates effortlessly got better than me at it very quickly; in particular I am convinced you don't need a Lean expert to be successful here).

First reason: I had easy access to undergraduates because I was teaching a compulsory 1st year undergraduate course and I would advertise the club in it. Are you sure that posters work? Can you somehow slide into their DMs? Are they on huge Whatsapp chat groups for example?

Second reason (absolutely key): I had a really interesting project which I was highly focussed on, namely "make this 30,000 line pile of triviality about finite sets called mathlib into something which contains some interesting undergraduate mathematics: for example, make the complex numbers, make matrices and prove that square matrices are a ring, prove quadratic reciprocity, develop field theory, prove insolvability of the quintic, prove that the derivative of sin(x) is cos(x) from the axioms of mathematics, prove e^{i.theta}=cos(theta)+i.sin(theta), prove that every natural number is the sum of 4 squares..." . This was really crucial: I had many projects, which ranged from easy to difficult, and students chose projects and self-assembled into small groups in order to solve them. I managed to instill into these students the importance of building an amazing mathematics library and, with the help of many other people from around the world, mathlib started turning into the thing which I was convinced that the mathematics community needed (even though at that time I was extremely unclear on exactly why it needed it). When it started to become clear that one could actually get publications out of our work I think that this became an even more exciting motivator for the students (about 5 of them ended up with publications as undergrads).

If you want to grow at Bristol (and for sure your undergrads are bright enough for this to be possible) then you might want to think about how to solve those two problems. The first is pretty easy to solve: you start asking undergraduates how to pass messages to everyone and you start asking those who teach big undergraduate classes if you can advertise something for 1 minute at the start/end of their lecture. The second one is more subtle: you have to decide what you're advertising. My experience from 2022 post-covid, where my message was "come to my Lean club, undergraduates, because Lean is kind of cool" was not coherent enough; 1st year undergraduates would show up, say "I want to contribute to mathlib" and I would say "oh crap, all that stuff that undergraduates were doing in 2018 is done now and basically what mathlib needs now is either a job for someone who's already a technical expert or involves graduate level algebra, which you don't know because you're a first year; personally I am becoming interested in proving FLT and you're not much help there either.". My message had become very weak and indeed the undergraduates stopped coming to the club, which is now basically a weekly social evening for graduate students and post-docs working in the area of formalization.

Laura, my impression is that you had some interesting formalization project ideas. You might want to consider a "launch event" where you give a lecture explaining a project and explaining how undergraduates can help, and stressing that this might well turn into a paper; also note that people are predicting that 2026 will be the year of the AI autoformalizer, which might get some people excited; a lot of kids are interested in AI, despite the fact that it currently writes crappy code. If you have a vision for a project or projects which are suitable for 1st years, which might lead to publications, and where you just feel like you need some extra hands, then I would focus on advertising that project/those projects and seeing what you get. At the end of the day there is ample evidence that a really good way to become a Lean power user is by working on a project and then having your code reviewed by someone else; forget the textbooks. If you are able to find a mathematically interesting project with parts which are accessible to undergraduates then this might be the hook for BLUE.

[Wrenna Robson]

Kevin Buzzard said:

I think that there were two reasons I was able to attract undergrads to my formalizing club in 2017 (when, let me stress, I knew very little myself about Lean and watched with interest as undergraduates effortlessly got better than me at it very quickly; in particular I am convinced you don't need a Lean expert to be successful here).

First reason: I had easy access to undergraduates because I was teaching a compulsory 1st year undergraduate course and I would advertise the club in it. Are you sure that posters work? Can you somehow slide into their DMs? Are they on huge Whatsapp chat groups for example?

Second reason (absolutely key): I had a really interesting project which I was highly focussed on, namely "make this 30,000 line pile of triviality about finite sets called mathlib into something which contains some interesting undergraduate mathematics: for example, make the complex numbers, make matrices and prove that square matrices are a ring, prove quadratic reciprocity, develop field theory, prove insolvability of the quintic, prove that the derivative of sin(x) is cos(x) from the axioms of mathematics, prove e^{i.theta}=cos(theta)+i.sin(theta), prove that every natural number is the sum of 4 squares..." . This was really crucial: I had many projects, which ranged from easy to difficult, and students chose projects and self-assembled into small groups in order to solve them. I managed to instill into these students the importance of building an amazing mathematics library and, with the help of many other people from around the world, mathlib started turning into the thing which I was convinced that the mathematics community needed (even though at that time I was extremely unclear on exactly why it needed it). When it started to become clear that one could actually get publications out of our work I think that this became an even more exciting motivator for the students (about 5 of them ended up with publications as undergrads).

If you want to grow at Bristol (and for sure your undergrads are bright enough for this to be possible) then you might want to think about how to solve those two problems. The first is pretty easy to solve: you start asking undergraduates how to pass messages to everyone and you start asking those who teach big undergraduate classes if you can advertise something for 1 minute at the start/end of their lecture. The second one is more subtle: you have to decide what you're advertising. My experience from 2022 post-covid, where my message was "come to my Lean club, undergraduates, because Lean is kind of cool" was not coherent enough; 1st year undergraduates would show up, say "I want to contribute to mathlib" and I would say "oh crap, all that stuff that undergraduates were doing in 2018 is done now and basically what we need now is either a job for someone who's already a technical expert or involves graduate level algebra, which you don't know because you're a first year". My message had become very weak and indeed the undergraduates stopped coming to the club, which is now basically a weekly social evening for graduate students and post-docs working in the area of formalization.

Laura, my impression is that you had some interesting formalization project ideas. You might want to consider a "launch event" where you give a lecture explaining a project and explaining how undergraduates can help, and stressing that this might well turn into a paper; also note that people are predicting that 2026 will be the year of the AI autoformalizer, which might get some people excited; a lot of kids are interested in AI, despite the fact that it currently writes crappy code. If you have a vision for a project or projects which are suitable for 1st years, which might lead to publications, and where you just feel like you need some extra hands, then I would focus on advertising those projects and seeing what you get. At the end of the day there is ample evidence that a really good way to become a Lean power user is by working on a project and then having your code reviewed by someone else; forget the textbooks. If you are able to find a mathematically interesting project with parts which are accessible to undergraduates then this might be the hook for BLUE.

Really really appreciate this advice.

[Wrenna Robson]

I am also starting to be convinced that AI probably has a role in all this - I mean it will whether we like it or not, but I mean from several directions. And I do think that is helpful.

[Wrenna Robson]

In terms of getting interest I mean.

[Kevin Buzzard]

This is not the place to talk about it, really, but my plan with FLT going forward is to farm off some 1980s parts of the proof to AI and continue with manual formalization for the more modern parts (esp the more modern definitions). So FLT might well be becoming more of a hybrid project. I think that for a proof you have to decide "do I want this to be done by a human or will I be content with it being done by a machine" and for FLT I am currently toying with the idea that I should offer up some of the 1980s stuff to AI companies; if their proof compiles, is crap, and then breaks after a mathlib bump and if AI can't fix it then who cares, I'll just go back to sorrying the result because I'm allowed to do that as part of the FLT project remit.

[Wrenna Robson]

That makes sense. I also think AI has a role for proof assistants that are, ah, less ergonomic than Lean. I am nominally employed on a grant doing EasyCrypt stuff but I've found it very challenging to grasp because of the nature of EC proofs.

[Wrenna Robson]

image.png

[Laura Monk]

Thanks @Kevin Buzzard for the advice! I do have a plan for some sort of Lean launch in Bristol, and have been collecting colleagues who would like to add it to the teaching curricular. Won't be quite yet but it is in the picture :)

[Wrenna Robson]

image.png
image.png

[Wrenna Robson]

I am not much of a web dev but I shall try to make a little page.

[Laura Monk]

Amazing! Let's start a poll for the next meeting, this way I have time to see it coming and advertise.

[Laura Monk]

/poll When would you be available for the next BLUE meeting?
Thursday 2nd April 10am
Thursday 9th April 10am
Thursday 23rd April 10am

[Freddie Nash]

My only thought is that it could be Bleu in honour of Bourbaki

[Laura Monk]

I guess if you read the square logo as a circle it is Bleu

[Freddie Nash]

Works for me!