The 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.
Due: 30 April 2027 · Weight: 20%
The brief#
Write a definition that the definition check accepts, then change it so that the check rejects it, and explain the difference.
In Metamath a definition is written the same way as an axiom. The Metamath Zero project’s README puts it plainly: “Definitions are just axioms in Metamath.” A verifier that checks proofs does not tell the two apart, so a definition that says more than it should goes unnoticed unless something else looks: set.mm’s verifiers page records that “definitions are checked by mmj2”. The week 7 lecture and lab are about that check; this exercise asks you to stand on both sides of it.
What you submit#
Three files: the database fragment with your good definition, the same fragment with the bad one, and the write-up. The lab says which database to build on and how to run the check.
How it is marked#
The two definitions are checked by the tool, and the check’s verdict is the mark for the first two criteria: a good definition that fails, or a bad one that passes, earns nothing for that criterion. The write-up is marked on whether it says, in plain words, what the bad definition would have let you prove.
The spec
The brief poses the problem and leaves room for a response. The spec is the fixed part: what a marker checks. Some lines can be checked mechanically; the rest call for judgement.
- a definition of your own that passes mmj2's definition check in the database the lab names
- a second version of it that fails the check, submitted alongside
- a write-up of no more than 500 words saying what the check found and what would have gone wrong without it
How it is marked
| Criterion | Weight |
|---|---|
| The good definition passes the check | 40% |
| The bad definition fails it, and you can say why | 40% |
| The write-up | 20% |