2025–2026, spring semester, NKUA Type-theoretic Foundations of Mathematics and Proof Assistants

Info

Prerequisites

• The only essential prerequisite is that enrolled students have time and will to study throughout the semester, attacking assigned problems and participating in class and in Zulip.
• About the so-called “mathematical maturity”: on one hand I assume that all enrolled students do have a minimum amount of it; on the other hand having too much of it can be a liability. The nature of this course might require the student to forget some practices/prejudices/notions that usually develop during classic mathematical studies.
• In particular, I do not assume that the enrolled students have taken courses like Mathematical Logic™ or Set Theory™. (But do not worry too much if you have.)
• Although a graduate course, undergrads are welcome to join after communicating their interest to do so (send me an email).

(Obs.: studying ≠ reading.)

Content

Objective / learning outcome

The student completing the course should:

1. understand the key notions of Type Theory and Proof Theory, and how they are used as a foundations for mathematics, including their role in developing formalization systems;
2. be able to use relevant tools and ideas from Category Theory and Order Theory;
3. understand the concept of mathematical proofs as a constructive/computational processes (programs), and propositions as types;
4. be able to formalize basic mathematical theories using a proof assistant;
5. understand dual or related concepts such as: syntax/semantics, dynamics/statics, intensional/extensional, specification/implementation, proposition/judgement, analytic/synthetic, type/set, etc.

Content summary

1. The concepts of definitions, propositions, and proofs. Examples from Algebra and Analysis.
2. Structural recursion/induction and its use as a means of giving definitions/proofs.
3. Elements of λ-calculus: anonymous functions and higher-order functions. The notion of a type. Inference rules of systems (for typing, proving, constructing, etc.)
4. Mathematical data types and structures: sets, tuples, products, sums, function spaces, algebraic and non-algebraic structures.
5. Elements of Order Theory and Category Theory: objects and constructions determined by universal properties, morphism properties, commutative diagrams. P(r)osets, lattices, Heyting Algebras and Boolean Algebras.
6. Martin-Löf Type Theories: elements of proof theory and dependent type theory, type families, Σ and Π types, constructive mathematics.
7. Programming with dependent types and formalization of mathematics with proof assistants (Lean, Agda).

Bibliography and references

Heard of Anna's Archive?

Bibliography

Lecture notes.

References

Category theory & Order theory

• Awodey (2010): Category Theory (2nd ed.)
• Goldblatt (1979): Topoi
• [CTCS] Barr & Wells (1998): Category Theory for Computing Science, 2nd ed., 2020 reprint
• Crole (1993): Categories for Types
• Riehl (2016): Category Theory in Context
• Davey & Priestley : Introduction to Lattices and Order
• Grätzer (1971): Lattice Theory: First Concepts and Distributive Lattices (Dover)
• Leinster (2014): Basic Category Theory
• Lawvere (1963): Functorial Semantics of Algebraic Theories
• Lawvere & Rosebrugh (2003): Sets for Mathematics

Type theory, Proof theory, Constructive mathematics

• Girard (1989): Proofs and types
• [HoTT] The Univalent Foundations Program (2013): Homotopy Type Theory
• Rijke (2022): Introduction to Homotopy Type Theory (CUP, 2022)
• Nordström et al (1990): Programming in Martin-Löf Type Theory
• Martin-Löf (1975): An Intuitionistic Theory of Types: Predicative Part
• Martin-Löf (1982): Constructive mathematics and computer programming
• Martin-Löf (1984): Intuitionistic Type Theory
• An intuitionistic theory of types, in G. Sambin, J. M. Smith (Eds.): Twenty-five years of constructive type theory, Oxford University Press, 1998, pp. 127-172.
• Bishop (1967): Foundations of constructive analysis
• Bishop, Bridges (1985): Constructive Analysis, Springer-Verlag.
• Bridges, Richman (1987): Varieties of Constructive Mathematics, Cambridge University Press.
• Mines, Richman, Ruitenburg (1988): A course in constructive algebra, Springer.
• Bridges, Vita (2006): Techniques of Constructive Analysis, Springer.
• Handbook of Constructive Mathematics (2023), Bridges, Ishihara, Rathjen, Schwichtenberg (Eds.), Cambridge, University Press.
• Veldman (2021): Intuitionism: an inspiration?
• Bauer (2017): Five stages of accepting constructive mathematics

Programming languages & Proof assistants (Lean, Agda, Rocq)

• [PFPL] Harper (2016): Practical Foundations for Programming Languages
• [FPIL] Christiansen: Functional Programming in Lean
• [TPIL] Avigad, de Moura, et al: Theorem Proving in Lean 4
• [MIL] Avigad, Massot: Mathematics in Lean
• Tao (2025): Lean formalization of Analysis I
• Escardó (2019): Introduction to Univalent Foundations of Mathematics with Agda
• Wadler, Kokke, Siek (2022): Programming Language Foundations in Agda
• Pierce, Azevedo de Amorim, Casinghino (2016): Software Foundations, Vol 1: Logical foundations
• Bird & Wadler (1986): Introduction to Functional Programming
• Hutton (2016): Programming in Haskell, 2nd ed.

Auxiliary

• Aluffi (2009): Algebra, Chapter 0
• Leinster (2012): Rethinking set theory
• Moschovakis (2005): Notes on Set Theory, 2nd ed.
• Wells (1993): Communicating Mathematics: Useful ideas from computer science (in American Mathematical Monthly, Vol 120, No. 5, pp.397–408)

Links

• NNG
• Lean
• The Missing Semester of your CS Education

Tools & technologies

Obs.: The list below may change during the execution of this course—except for the first item. (Install and/or create an account where necessary.)

1. PEN(CIL) and PAPER (may be digital).
2. Zulip (read the FAQ).
3. The proof assistant Lean.
4. The functional programming language Lean (yes, it is the same thing).
5. Git.
6. Recommended but not necessary: some Unix-based system.
7. Very recommended: sooner or later you will need to write a lot of special unicode characters like ∀, ∃, ⊃, etc.
   (It is the year 2026, this should not be too scary.)

Rules

This is a MSc-level course. I expect/hope that I do not need to state rules; hopefully this section will continue rule-free till the end.

Student duties

1. Visit this site and Zulip regularly (preferably on a daily basis). (Anything posted here or on Zulip will be considered to be known by all enrolled students.)
2. Study and attempt to solve the hw (especially those you cannot solve).
3. Participate on Zulip by sharing your answers to get feedback, and by checking your peers solutions and questions to offer your input.
4. Participate in the lectures! Obs.: when you have a question during class, just raise your hand and wait. Do not wait till the end of the class to ask your question “in private”! (Most of the times that this happens I will ask the student to post their question on Zulip or to ask it during the next class.)

About cheating

1. Do not.

Cellphones vs notes

There is not much sense in showing up without some means to take notes. Also keep your cellphones silent/airplane-mode/off. No need to take photos of the board: all of it will be available online soon after each class.

Grading

Disclaimer. I assume that the students enrolled in this class did so out of interest on the subject. Ideally one should ignore irrelevant matters like grades and exams. Focus on studying and participate in the mathematical “fights” during classes as well as online on Zulip. Dive in! 🤿

Still, the final note will be based on one or more of: (i) participation; (ii) solved hw; (iii) written exam; (iv) take-home exercise sets.

Each student is responsible for their own note-taking and organization of the subject.

FAQs

• Zulip
• Install

(More to be added soon.)

Dynamic content

Exams

No exams scheduled yet.