Student logic seminar (both 2021/22 semesters):
Sources, schedule and slides
Sources:
all papers available below are freely available on the web and are
meant for the study purposes and not for further distribution.
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.