Events | Bristol Lean Users and Enthusiasts

Upcoming events

BLUE community meetings

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!

Lean mini-course by Patrick Massot

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 formalise mathematics in 2027? by Patrick Massot
16 - 17	Abstract A 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 - 12	Independent talks on different aspects of Lean
11 - 12	Tuesday: What kind of mathematics do we learn while formalising? Abstract Encoding mathematical definitions, statements, and proofs in a computer language requires adapting one's way of thinking. Of course, there is a formal adaptation dictated by the software's syntax and the logical foundations used. However, this presentation will focus on the purely mathematical aspects. I will present several sets of elementary examples showing how abstractions motivated by formalisation can simplify statements and proofs. There are no prerequisites in formal mathematics, and I will not show a single line of computer code. Wednesday: An introduction to logical foundations of Lean Abstract Like ordinary mathematics, formalised mathematics mostly don't require to think about logical foundations. But it can still be occasionally useful to know how Lean's logical foundations allow to encode mathematics. And it's also arguably pretty interesting to get a glimpse of an unusual way of doing this where logic, proofs and mathematical objects are gathered in a unified context. This will be a mind bending but very elementary talk. Thursday: More advanced talk depending on interest during tutorials
12 - 13:30	Lunch
13:30 - 15:30	Lean tutorial sessions
13:30 - 15:30	Details You 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: Teaching mathematics using Lean
12 - 13	Abstract Since 2019, I've been using Lean to teach precise mathematical reasoning to first year undergrads in Orsay. Along the way, I developed Verbose Lean, a set of tools built on top of Lean that offers a syntax that is easier to transfer to paper, and more control on what the software can or cannot do automatically. In this talk I will show what it looks like and emphasize the flexibility it brings to teachers. This flexibility allows to tune the amount of help given to students and the level of precision required from them. Discussion is welcome.

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.