Student logic seminar (both 2021/22 semesters):
Sources: all papers available below are freely available on the web and are meant for the study purposes and not for further distribution.
Sources, schedule and slides
Schedule (for both semesters) and slides from some seminar talks are available at the bottom (some talks were interactive).
Informal texts painting some background or motivations
J.Avigad's papers:
- Automated reasoning for the working mathematician,
- The mechanization of mathematics,
- Varieties of mathematical understanding.
J.Avigad and J.Harrison: Formally verified mathematics
M.Nathanson, Desperately seeking mathematical truth
P.Scholze's Liquid Tensor Experiment: blog post and an article in Nature
V.Voevodsky's Univalent Foundations:
- 2014 IAS lecture (and his lecture page),
- The origins and motivations of univalent foundations,
- Univalent Foundations page
IAS Univalent Foundations page
Logic background (will grow)
Logic and Proof (form the Learn Lean page),
introduction to propositional and first-order calculi: Chpt.2 in van den Dries's LN,
introductions to lambda calculus: by H.Barendregt and E.Barendsen or R.Rojas,
introductions to type theory: by D.Christensen or by H.Geuvers.
Lean (sources suggested by J.Avigad)
An overview of resources: Learning Lean
The standard reference for the dependent type theory and the syntax of the system:
Theorem Proving in Lean
(a thorough treatment of the basics, but it doesn't say much about the mathematical library).
Natural Number Game by K.Buzzard and M.Pedramfar: online interactive tutorial focused on proving properties of the elementary operations on natural numbers.
For mathematical library: Mathematics in Lean
(under construction, but there are about 50 pages there)
Online (pandemic) workshop
that was designed to introduce mathematicians to Lean (materials and YouTube videos of the lectures are available).
People on the Lean Zulip channel are welcoming and helpful, and students are welcome to introduce themselves there and ask questions.
Isabelle (sources suggested by S.Holub)
T.Nipkow's basic tutorial
Isabelle documentation page
Basic logic background: L.C.Paulson's paper
For more sophisticated issues: T.Nipkow-S.Roskopf's paper or O.Kuncar-A.Popescu's book chapter.
S.Holub runs a seminar on formalization in Isabelle.
Winter schedule (and slides)
8.X.21, Jan Krajicek, A mathematical logic perspective of the topic
15.X.2021, Mykyta Narusevych, Introduction to type theory, after Geuvers - see above
22.X.2021, Begaiym Adylbek, Theorem Proving in Lean - 1 (or .pptx version), after the text book listed above
5.XI.2021, Filip Bartek, Theorem Proving in Lean - cont'd, an interactive talk using the textbook
12.XI.2021, Martin Raska, Theorem Proving in Lean - cont'd, slides (plus an interactive presentation)
19.XI.2021, Jiri Rydl, Theorem Proving in Lean - cont'd, slides and code
26.XI.2021, Mykyta Narusevych, Theorem Proving in lean - cont'd, code
3.XII.2021, Martin Melicher, Theorem Proving in Lean - con't, code,
10.XII.2021, Begaiym Adylbek, Logic and Proof, pdf and pptx.
17.XII.2021 (prepared but not presented), Claudia Ligonie Lerma, Univalent Foundations, slides.
Summer schedule (and slides)
18.II.2022, organizational meeting and Jan Krajicek, The existence of infinitely many primes in Peano arithmetic,
25.II.2022, Mykyta Narusevych, a recapitulation of first three chapters in the textbook,
4.III.2022, Martin Raska, a review of Chpt.4,
11.III.2022, Jiri Rydl, Chpt.5, code,
18.III.2022, Martin Raska, Chpts.6(brief) + 7, code,
25.III.2022, Mykyta Narusevych, Chpt.7 cont'd, code,
1.IV.2022, Jiri Rydl, Chpt.7 (7.3-->) cont'd, code,
22.IV.2022, Jiri Rydl, ex.: infinitude of primes, code,
29.IV.2022, Martin Raska, elementary proof of the infinitude of primes,
6.V.2022, Martin Raska, con't from 29.IV., code.