Hauptseite

News

Poster Session

Written on 30.01.26 by Leon Pernak

Dear participants,

Next week, on Thursday, Feb. 5th will be the poster session. It will start at 14:00 (s.t.!) and happen right outside the usual lecture hall HS I. Bring your printed posters and hang them in one of the free spots. Alex and me will walk around and have a quick (5-10min)… Read more

Dear participants,

As already explained, the content of the poster should be your project, with a lot of freedom. You may find inspiration in the following questions: What is the theory you are formalizing (mathematically)? Are there applications/reasons why it's important to formalize them? Which concepts in Lean/mathlib are you going to use? Are you planning on specific models for some definitions?

Poster size should be either DIN A2 or A3. Posters can be hand-written/-drawn or printed (or anything else, really, if it supports the presentation). Please have the names of all group members on the poster.

During the session, you are highly encouraged to look at the other posters and discuss amongst each other - that's what the session is intended for.

See you there,

Leon

Guest Talk and Research Seminar Talk by Rida Hamadani

Written on 23.01.26 (last change on 24.01.26) by Leon Pernak

Dear participants,

I'm happy to inform you that next week's seminar session will feature a guest talk by Rida Hamadani, about their extensive experience in using Lean both in the mathematical community as well as professionally in the industry.

In addition to the talk in the seminar, Rida will… Read more

Dear participants,

In addition to the talk in the seminar, Rida will give another talk on formalizing specific algebraic topics in Lean, in the Research Seminar of the algebra group, where everybody who is interested is very welcome. This talk will be on Tuesday (27th) at 14.00 (sharp) in HS IV in building E2.4.

Title and abstract of that talk will be published over the next couple days here.

Have a nice weekend,

Leon

PS: While I promised to share a link to the university poster latex templates, it seems like these are no longer publicly available. However, a quick websearch is going to provide you with plenty of other examples, and I suppose GenAI is reasonably good at LaTex these days ;)

Git template for project/Forum/Instructor mails

Written on 19.01.26 by Leon Pernak

Dear participants,

There is now a git repository with a project template for your seminar project, to be found here: https://gitlab.cs.uni-saarland.de/pernak/fmil26

For your individual project you should fork the project above. Read the Readme file in the root folder for further instructions on… Read more

Dear participants,

There is now a git repository with a project template for your seminar project, to be found here: https://gitlab.cs.uni-saarland.de/pernak/fmil26

For your individual project you should fork the project above. Read the Readme file in the root folder for further instructions on how to structure your files.

Also, once you have created the project add me (@pernak) to the repository as a reporter. If Alex is your project instructor, add him (@alik00001) too.

If Alex is your instructor, you can now also find his E-Mail on the "Team" page in CMS.

Lastly, there is now a Forum on the CMS Page. You can use it to find project partners or share inspirations for projects, and ask questions.

Happy leaning, see you on Thursday.

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 verication. 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.