Collaborative Seminar on "Lean 4"

This seminar is a collaborative and exploratory space for learning Lean 4 and understanding its foundations in Dependent Type Theory.One goal of the seminar is to gain understanding on how to formalize proofs in Lean 4. Beyond this we study the deeper context of Lean 4 by exploring the intersection of dependent type theory, computability theory, proof theory, logic, and category theory.We want to explore both its practical use and its conceptual underpinnings.

Upcoming session(s):

13. Mai 2026 · 14:15 – 15:45 Uhr

13. Mai 2026 14:15 – 15:45 Uhr

Regular Session

Plan for next session:

We currently read parts of the Homotopy Type Theory bookExterner Link.
Until the next session: Please read Sections I.1.3 until including I.1.5 i.e. the sections on Universes and families, Dependent function types and produt types until the next session

Information

The seminar is open to participants of all backgrounds, the seminar thrives on curiosity, discussion, experimentation, and shared reflection.

Please join the mailing list to receive updates and invitations:
https://lserv.uni-jena.de/mailman/listinfo/lean-seminarExterner Link

The regular sessions will always take place in Room 1085, Inselplatz 5Externer Link.
They may be scheduled irregulary, as we share the seminar room with the PhD-seminar, so subscribe to the mailing list or check the above list of upcoming sessions.

Materials of the Lean Seminar

1. WhyNotFirstOrderLogic.pdf
  en
  The slides for a talk on the question "Why doesn't Lean just use First Order Logic as its Foundation".
  
  Dateityp:
  
  pdf
  
  Dateigröße:
  
  140 kb
  
  Änderungsdatum:
  
  24. April 2026
  
  Erstellungsdatum:
  
  24. April 2026
  
  Datei herunterladen

Auxiliary Material

What Is Lean 4?

Lean 4 is an interactive theorem prover — a software tool that allows mathematical definitions, statements, and proofs to be written in a formally precise and machine-verifiable way.
It brings together ideas from logic, type theory, and programming, enabling us to explore mathematics with explicit formal rigor.

Lean is used in formalizing mathematical theories, developing verified proofs, and deepening understanding of foundational concepts in logic and computation.

What Are We Doing?

This seminar is designed as a shared learning project rather than a lecture series with designated experts.
All participants, whether new to theorem proving or with prior experience, are welcome.

Our initial focus will be on:

Reading and working through “Theorem Proving in Lean 4”, a hands-on introduction to Lean.
Playing the Natural Numbers Game (https://adam.math.hhu.de/Externer Link), an interactive Lean exercise that teaches basic proof techniques through practice.

As the group progresses, we plan to organize short presentations on theoretical foundations relevant to Lean and formal reasoning, such as:

Simple type theory
Dependent type theory (DTT)
Curry-Howard correspondence
relationship between DTT and first order logic (FOL)
relevant aspects of FOL

Learning Together

The guiding philosophy of this seminar is:

Shared exploration and discussion
Collaborative problem solving
Building intuition and understanding
Making and learning from mistakes

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

How to Join

If you are interested in participating or would like more information, please subscribe to the mailing list:

https://lserv.uni-jena.de/mailman/listinfo/lean-seminar

Alternatively, you may send an email with the subject line “subscribe” (and no further content) to:
lean-seminar-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.

Contact

Jamal Paul Drewlo

Organisator

Professur für Ergodentheorie und Dynamische Systeme

E-Mail: jamal.drewlo@uni-jena.de
Telefon: +49 3641 9-46231
Link zum Herunterladen der vCard: vCard

Raum 1053
Inselplatz 5
07743 Jena Google Maps – LageplanExterner Link

weiterführender Link: Zur WebseiteExterner Link

Lino Joss Fidel Haupt