What is covered, week by week, and which topics each lecture draws on.
One lecture a week, on Mondays. Each page says what the lecture covers, links every source it draws on at the sentence that uses it, and ends with the reading for the week. Wednesday’s lab picks up where the lecture stops.
What Metamath is, and where it lives
Metamath in the project's own words: the language, the website and its mirrors, the licence, the GitHub organisation, and three unrelated projects that share the name.
Week 1 · 22 February 2027
The language
What a .mm file is made of: the four-page specification in the Metamath book, a condensed introduction, two machine-readable grammars, and the $j annotations that tools read.
Week 2 · 1 March 2027
Verification
What a verifier does, the five verifiers that check every change to set.mm and the workflow that runs them, the conformance suites, and how many more verifiers exist.
Week 3 · 8 March 2027
set.mm and the Proof Explorer
The set.mm database, the web pages generated from it, the theorem list as its table of contents, how it cites books, and where its history is kept.
Week 4 · 15 March 2027
Proof assistants
The tools a student proves with — mmj2, metamath-lamp, Yamma, mmt1, metamath-exe's own assistant — and how they differ from the verifier you will write.
Week 5 · 22 March 2027
The axioms, and the metalogic behind $d
Where set.mm's axioms come from, why its statements are schemes rather than theorems, what a distinct-variable condition is, and the results and open problems around them.
Week 6 · 29 March 2027
Definitions and soundness
A Metamath definition is an axiom to the verifier, so a wrong one can make the database inconsistent without any proof failing. What the extra check is and which tool runs it.
Week 7 · 19 April 2027
Other databases
The Metamath databases beside set.mm: intuitionistic logic, higher-order logic, New Foundations, quantum logic, Peano arithmetic, the MIU system, Laws of Form, and the third-party ones on GitHub.
Week 8 · 26 April 2027
Formalisation in practice
What large Metamath proofs cost, from the ones that exist: GCH implies AC, the prime number theorem, Bertrand's postulate, a proof done on video, legibility research, and the 100 theorems scoreboard.
Week 9 · 3 May 2027
Descendants, translations and comparisons
The languages that grew out of Metamath, the programs that carry proofs into and out of it, and one published comparison that sets it beside sixteen other provers.
Week 10 · 10 May 2027
Machine learning on Metamath
The papers that trained programs to find Metamath proofs, in order from 2016 to 2025, the datasets and tools built for them, and a name collision to know about.
Week 11 · 17 May 2027
Miscellanea
The pieces that fit nowhere else: the Solitaire applet, the shortest Principia proofs, open problems, where the community talks, meetings, a video, the GitHub organisation, and one paragraph of history.
Week 12 · 24 May 2027