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.
Due: 21 May 2027 · Weight: 30%
The brief#
Prove the theorem the lab sets, and hand in the proof.
Every lab from week 3 to week 11 ends with a theorem to prove in mmj2, usually started in the room and finished afterwards. The theorem is chosen so that the week’s lecture is what you need to prove it, and so that the proof takes an hour, not an evening. The best eight of the nine count, so one bad week costs nothing.
What you submit#
The proof file the lab names, by 5pm on the Friday of that week, through the course submission page. Nothing else: no write-up, no screenshot.
How it is marked#
A proof that the verifier accepts gets the first 80% of the marks for that week. The remaining 20% is for a proof a person can read: steps in an order that follows the argument, no unused steps, and hypotheses named as the lab asked. A proof that does not verify gets no marks that week, whatever else it has; that is the whole point of the subject, and it is also why the best eight count rather than all nine.
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.
- each proof verifies in mmj2, against the database the lab names, with no errors
- each proof is submitted as the file the lab names, by 5pm on the Friday of its week
- the best eight of the nine proofs count, each for one eighth of the mark
How it is marked
| Criterion | Weight |
|---|---|
| The proof verifies | 80% |
| The proof is readable | 20% |