| Home | Events | Projects | Members |
The School of Mathematics of the University of Bristol hosts
regular informal meetings for BLUE, in the Fry Building (BS8 1UG).
They take place roughly every other month
and are an opportunity to meet people interested in Lean in the local area,
and get some help from experienced users.
Participants are given the option to give a 5-10 minute presentation of their recent projects if they wish to.
Meetings are currently on hold. Please reach out if you'd like to organise them!
We are organising a week-long Lean event in Bristol from 26 to 30 October 2026. The key event will be a 3-day long mini-course on Lean by Patrick Massot. External participants are welcome, and there will be a small amount of funding available for young participants.
| Monday | ||
| 16 - 17 | Colloquium: Why formalising mathematics in 2027? by Patrick Massot | |
AbstractA growing number of people are having fun explaining mathematics to computers using proof assistant softwares. This process is called formalisation. In this talk, I’ll show what formalisation looks like, describe what kind of things it teaches us, and how it could even turn out to be useful. This landscape is rapidly changing as part of the global generative AI disaster, so I will also include a discussion of how I hope those activities can stay relevant in 2027 and beyond. |
||
| 17 - 18 | Wine reception | |
| Tuesday - Thursday | Lean 4 mini-course by Patrick Massot | |
| 11:30 - 12:30 | Independent talks on different aspects of Lean, titles TBA | |
| 12:30 - 14 | Lunch | |
| 14 - 16 | Lean tutorial sessions | |
DetailsYou will be offered an introduction to Lean through a hands-on practice tutorial. You are welcome to join the sessions at any time, according to your own availabilities: different activities will be offered depending on the amount of time you are able to commit. Patrick Massot and a few other Lean users will be available to set you up and answer all your questions. |
||
| Friday | ||
| 12 - 13 | Maths Education seminar: How to include Lean in our teaching practices? | |
We thank the Heilbronn Institute for Mathematical Research for funding this event through their International Visitor Scheme. Registration is open until September 30 on this link.