Jonas Bayer

Outreach

Lean Workshop

This section contains material for the Lean workshop at the event UK welcomes Studienstiftung.

Schedule

Material for mini-projects

Project A: Beyond the Natural Number Game

What's your favourite (undergraduate-level) theorem in mathematics? The idea of this mini-project is to explore how a theorem of your choice is formalised in Lean. You can use the search bar in the Mathlib documentation and refer to search tools listed below. Probably, what you get out of this won't make a lot of sense at first. Take a look at the book Mathematics in Lean to learn more about how to do formalisation beyond the Natural Number Game.

Project B: A New Understanding of Mathematical Proof

How does formalisation with tools like Lean change how we view mathematical proofs? Or does it not? The idea of this mini-project is to analyse how the adoption of formalisation in mathematical research can change the conception of what constitutes a proof. The material below focuses on perspectives from mathematicans and computer scientists. If you have a background in philosophy: how do various philosophers think about the concept of mathematical proof? Can you find literature on the topic and make a comparison?

Project C: Lean meets AI

Recently, Lean has played an important role in the development of AI systems for mathematics. How do these AI systems work? What are their limitations? And how does Lean come into the picture? The mini-project is to shed light on these questions by analysing the examples linked to below. Note that, recently, a lot of work has focused on solving problems from the International Mathematical Olympiad (IMO). These problems can be explained to anyone with a high-school level understanding of mathematics but are very challenging to solve, requiring multi-step reasoning.