News
LSF registration/DeadlinesWritten on 11.11.25 by Leon Pernak Dear students, Since multiple people asked recently: The seminar has not yet been added to the examinations in LSF, so you cannot officially register for it yet. This will happen in due time (~ early December) in accordance to all guidelines by the informatics and math departments. I'll inform… Read more Dear students, Since multiple people asked recently: The seminar has not yet been added to the examinations in LSF, so you cannot officially register for it yet. This will happen in due time (~ early December) in accordance to all guidelines by the informatics and math departments. I'll inform and remind you to register once the entries have been set up. See you Thurdsday, Leon |
Mathematics in LeanWritten on 06.11.25 by Leon Pernak Dear participants, Todays materials are online. Until next week, please Finish the NNG if you haven't yet. Install Lean and VSCode (or another suitable editor of your choice) on your machine Clone the Mathematics in Lean repo, and open it in VSCode to initialize/compile. You can do so… Read more Dear participants, Todays materials are online. Until next week, please Finish the NNG if you haven't yet. Install Lean and VSCode (or another suitable editor of your choice) on your machine Clone the Mathematics in Lean repo, and open it in VSCode to initialize/compile. You can do so by cloning the repository via git, or hitting the universal quantifier button in VSCode (upper right), choose Open Project - > Download Project -> Choose suggestion Mathematics in Lean. The repository takes a while to download and compile, so please do this before next weeks seminar. All the best, 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.