Formal Mathematics and Proof Assistants (2022)

Discussion Board

The discussion board is ready: http://164.92.203.204/punbb-1.4.6/index.php
Please register but do not use any information you wish to keep private. (The board is not under https.) Use a fake email like (fakeemail@trash-mail.com) and do not use a password you use anywhere else.

Online Material

The Schroeder Bernstein Theorem with formal exercises in higher-order set theory.
An introduction to higher-order set theory in Megalodon, with a partial proof of Schroeder Bernstein in to be completed by the student. You can either install Megalodon yourself or do the exercises online at the links below.
A few simple basic logic exercises in Megalodon: Three parts of Megalodon exercises leading up to and including the proof of Schroeder Bernstein (after March 8 2022):

A partial formalization of Schroeder Bernstein Coq is available here. You should be able to compare and contrast the partial Coq version with the partial Megalodon version to (1) get an idea of the difference between type theory and set theory and (2) get an initial idea of how to make definitions and prove theorems in Coq. We will say more about Coq later in the course and then ask you to complete the proof of Schroeder Bernstein in Coq. Questions about the Coq version are welcome on the discussion board.

The webpage for the 2017 course.