BerLean: learning group on formal mathematics

Are you wondering what the recent excitement about Lean is about? What the formalisation of deep theorems (such as the liquid tensor experiment, sphere eversion or the unit fractions project) means? Why we would be interested in doing this? You have a chance to find out!
In summer 2024, we're organising an informal learning group about formalised mathematics and the Lean theorem prover. By attending, you will

• learn about the current state of formalising mathematics
• get an impression how formalising feels
• have the chance to formalise some mathematics yourself

No matter if you just want to get an idea of Lean, get your toes wet or dive right in and formalise some mathematics nobody has formalised before: all of these will be possible, and we are happy to help you on the way!

Organisational details

We'll start with a one-day-workshop to get a first impression. If there is interest, we can have another one-day workshop, meet more regularly or do whatever suits your interests best.

Date and time: Friday, May 10, 9.30–17.00 (with lunch and breaks)
If you cannot attend the workshop on this day; feel free to reach out to me — we may do a second workshop and would be happy to have you join!
Location: room 1.023, Johann-von-Neumann-Haus
in the HU math department, Rudower Chausee 25, 12489 Berlin
about 10 minutes by foot from S-Bahnhof Adlershof
Tentative schedule:

• 09.30. Welcome and motivation
• 10.00. Overview of Lean
• 11.15. Short break
• 11.30. Natural number game; installing Lean
• 12.45. Lunch break
• 13.30. Logic and basic tactics
• 14.45. Coffee break
• 15.15. Parallel sessions, topics depending on interest
• 16.30. Wrapping up and outlook

Organizers: Yves Jäckele (TU Berlin), Michael Rothgang (HU Berlin) and Nicolas Weiss (HU Berlin)
All of us have some experience in Lean, but we're also still learning: there are no stupid questions; you're welcome without any knowledge of Lean.