News
Room change/Materials/First sessionWritten on 16.10.25 by Leon Pernak Dear Participants, To remind everybody (and myself): Next weeks meeting is going to be in Lecture Hall 1 (E2.5) again. I also uploaded todays slides to the materials section. For those who couldn't attend todays session: Take a quick look at the slides, and try to complete all levels up to… Read more Dear Participants, To remind everybody (and myself): Next weeks meeting is going to be in Lecture Hall 1 (E2.5) again. I also uploaded todays slides to the materials section. For those who couldn't attend todays session: Take a quick look at the slides, and try to complete all levels up to the end of "Addition world" in the Natural Number Game. See you next week, Leon |
Formalizing Mathematics in LEAN
This is the course page for the seminar and proseminar "Formalizing Mathematics in LEAN".
Time: Thursdays 2pm c.t. (subject to change)
Location: HS I (E2.5)
First Meeting: Oct. 16th 2025
Please bring a laptop if possible, or if not, send me an email ahead of time.
L∃∀N (lean) is a modern theorem prover and functional programming language that allows
mathematicians to write formal proofs with computer veri cation. It is increasingly used in
the mathematical community, where the applications range from verifying high-level research
mathematics like the Liquid Tensor Project to experimenting with how far AI can take us in
writing mathematical proofs.
Seminar Contents
The seminar will give a gentle introduction to the L∃∀N theorem prover, learning its syntax,
concepts, and how to use it to formalize your own proofs.
We will start by doing the exercises in the Natural Number Game, a beautiful hands-on tutorial that introduces the basic concepts. After that, we will go through some parts of the Mathematics in LEAN textbook and its exercises.
After that the main goal is that each participant finds their own personal project to formalize in LEAN, either some mathematics you are interested in that you saw in a lecture, something in theoretical computer science, or whatever else comes to mind. The final grade of the seminar will be based on this project, which can be completed after the semester finishes, and possibly a short presentation in the seminar, depending on time and number of participants.
Prerequisites
Neither mathematical background nor programming experience is required to participate in the
seminar, and students new to both mathematics and computer science are very much encouraged
to participate, but more experienced students in either topic can also be sure to nd challenges
at their level.
Workload and Examination
Your main contribution for the seminar is going to be your individual project. As a guideline, if you're taking the course as a Proseminar, your project should be realizable in about 60h, for Seminar about 90h. The grading will be based on three things:
- The Lean project code
- Documentation of your project, which is
- Documentation of the mathematical contents of the project (1 page Proseminar/3 pages Seminar)
- Documentation of the Lean code (1 page Proseminar/2 pages Seminar)
- A poster about your project, summarizing both the math and the Lean ideas behind it.