Metamath from nothing: the language, the programs that check it, the set.mm database, and proving in mmj2. Twelve weeks of lectures and labs, ending in a proof verifier you wrote yourself.
What you will do
Learn to read a Metamath database, prove theorems in it, and write a program that checks the proofs. Each week has a Monday lecture and a Wednesday lab. The first two labs install the tools and read small databases; from week 3 every lab ends with a theorem to prove in mmj2, and a proof counts when the verifier accepts it. From week 5 you are also writing your own verifier, in a language of your choice, marked against a test suite the course provides.
Who it is for
Anyone who wants to learn Metamath. You need to have programmed before, in any language, because the verifier project is a program. You do not need to have studied logic: the language is taught from nothing in the first three weeks, and every symbol is explained when it first appears. If you have met formal logic already, the first three weeks will be quick and the rest will not.
Where to go next
Lectures
What each of the twelve weeks covers, and the reading behind it.
Labs
What to bring to each lab, what happens in it, and what leaves the room.
Assessment
Lab proofs, the definition exercise and the verifier project: what each is worth and when it is due.
People
Who teaches the course and who to ask about what.