# Site

## Pages

- [Page not found](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/404/): That page doesn't exist, or it has moved since you last looked
- [Assessment](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/assessments/): Every piece of graded work in the course, what it is worth, and when it is due.
- [The definition exercise](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/assessments/definition-exercise/): Write a definition, break it, and explain what the definition check caught. Set in week 7, due at the end of week 8.
- [Lab proofs](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/assessments/lab-proofs/): Nine weekly proofs, weeks 3 to 11, each due on the Friday of its week. The best eight count, and a proof counts when the verifier accepts it.
- [The verifier project](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/assessments/verifier-project/): Write your own Metamath verifier, in a language of your choice, and have it marked against a test suite the course provides. Set in week 5, due at the end of week 12; full details to follow.
- [Lectures](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/): What is covered, week by week, and which topics each lecture draws on.
- [What Metamath is, and where it lives](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-01/): 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.
- [The language](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-02/): 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.
- [Verification](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-03/): 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.
- [set.mm and the Proof Explorer](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-04/): 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.
- [Proof assistants](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-05/): 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.
- [The axioms, and the metalogic behind $d](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-06/): 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.
- [Definitions and soundness](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-07/): 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.
- [Other databases](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-08/): 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.
- [Formalisation in practice](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-09/): 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.
- [Descendants, translations and comparisons](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-10/): 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.
- [Machine learning on Metamath](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-11/): 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.
- [Miscellanea](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/lectures/week-12/): 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.
- [People](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/people/): Who teaches the course, and how to reach them.
- [Noor Castellane](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/people/noor-castellane/): Convenor. Gives the Monday lectures, sets the assessments, and is the person to ask about anything that is not a lab.
- [Teodor Ashby](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/people/teodor-ashby/): Tutor. Runs the Wednesday labs, marks the lab proofs, and is the first person to ask when a proof will not go through.
- [Policies and support](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/policies/): The course-wide rules: deadlines and extensions, working together, the use of tools, what you may do with what you produce, and where to get help.
- [Install and verify](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/01-install-and-verify/): Get metamath-exe and mmj2 running on your own machine, download set.mm, and watch a verifier check every proof in it.
- [Read a small database, write a smaller one](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/02-read-and-write/): Read miu.mm and peano.mm line by line, then write a database of about ten lines by hand and get a verifier to accept it.
- [First proof](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/03-first-proof/): The first proving lab: build a short propositional-logic proof in mmj2's Proof Assistant, unify it, and see the verifier accept it. This lab counts toward the lab-proof mark.
- [Navigate and prove](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/04-navigate-and-prove/): Find a theorem in the Proof Explorer and read its proof step by step, then prove a propositional theorem of your own in mmj2 with set.mm loaded.
- [mmj2 in depth](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/05-mmj2-in-depth/): How mmj2 unifies a step, what a work variable is for, and how to grow a proof worksheet one step at a time until a theorem that needs several steps verifies.
- [Distinct variables](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/06-distinct-variables/): Prove a theorem whose proof needs a $d condition, then remove the condition and read the error the verifier reports.
- [A definition that fails](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/07-a-definition-that-fails/): Add a definition to a copy of set.mm, run mmj2's definition check, watch it reject one, and fix it. The corrected definition starts your definition exercise.
- [Prove in iset.mm](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/08-prove-in-iset/): The same theorem proved against set.mm and then iset.mm, to see where a classical proof needs excluded middle. Then the verifier project check-in: where your verifier should be by now.
- [A longer proof](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/09-a-longer-proof/): Plan a proof that needs several lemmas before typing any of it, then prove the lemmas in order in mmj2 and verify the whole file in metamath-exe.
- [Read MM0 against Metamath](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/10-read-mm0/): Read the Metamath Zero translation of set.mm's axioms beside the axioms themselves, line by line, and say what each file states that the other leaves out.
- [Verify a machine-found proof by hand](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/11-verify-by-hand/): Take a short propositional proof found by exhaustive search, check every step on paper, then check it in mmj2 and with mmverify.py. The last lab that counts toward lab proofs.
- [Retrospective](https://comp4020-agentic-coding-studio.github.io/comp4020-ass2-amackay/sessions/12-retrospective/): Demonstrate your verifier on peano.mm and on a file you have not seen, then show one proof from the semester. The last lab; the verifier project is due this week.