Lean 4 Seminar and Lean Colloquium

The seminar is designed as a shared learning project. It is not a lecture series with designated experts.
All participants, whether new to theorem proving or with prior experience, are welcome.
We deliberately take on topics in which none of us has prior expertise and work through them together. This makes the seminar demanding, but also very rewarding.
Everyone is welcome, whether new to theorem proving or experienced.

We read the introductory section on Dependent Type Theory of the Homotopy Type Theory BookExterner Link.
We then deepened our understanding by teaching us in-depth the syntax and meta-theory of

• Lambda Calculus
• Simply Typed Lambda Calculus (with and without type formers for the empty and unit type as well as for sum and product types).

Furthermore, we studied the basics of the meta-theory of

• System F, and
• Martin-Löf Type Theory.

This included sessions regarding

• Strong Normalization and Canonicity
• Curry-Howard correspondence
• relationship between DTT and first order logic (FOL)
• relevant aspects of FOL

In the colloquium, seminar members present material the seminar has taught itself, in a consolidated and more accessible form. Still, the speakers are not experts on their topics. They are participants who have worked through the material together and now share what they have understood.

The talks are aimed at a mathematically experienced audience. They should be accessible to anyone with a Bachelor’s-level background in mathematics, or in logic and theoretical computer science. The discussion afterwards is free to go into depth, so not every part of it will be accessible to everyone, and questions at every level are welcome.

Sessions take place irregularly, whenever a topic is ready.
You can join the announcement-only mailing list for the Colloquium hereExterner Link.

The guiding philosophy of both the seminar and the colloquium is:

• Shared exploration and discussion
• Building intuition and understanding

In the seminar we additionally put an emphasis on

• Collaborative problem solving
• Making and learning from mistakes

We do not assume expertise at the outset;
rather, we learn together and support each other in developing proficiency.

If you are interested in participating or would like more information, please subscribe to (one of the) the mailing lists:
Seminar: https://lserv.uni-jena.de/mailman/listinfo/lean-seminarExterner Link
Colloquium: https://lserv.uni-jena.de/mailman/listinfo/lean-colloquiumExterner Link

Alternatively, you may send an email with the subject line “subscribe” (and empty body) to:
Seminar: lean-seminar-request@listserv.uni-jena.de
Colloquium: lean-colloquium-request@listserv.uni-jena.de

We welcome anyone with curiosity about formal theorem proving, type theory, or the computational foundations of mathematics.

We look forward to learning together and hope to see some of you tomorrow or in future sessions.