News
Currently, no news are available
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 IV (E2.4)/some online meetings later on
First Meeting: Oct. 16th 2025
Please bring a laptop if possible, or if not, sent 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.