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.

Policies and support#

Deadlines and extensions#

Lab proofs are due by 5pm on the Friday of their week. The definition exercise and the verifier project have their own due dates on their pages. Work submitted after a deadline without an extension is not marked. Ask before the deadline and an extension is granted for the asking: email the convenor with the date you can meet. After the deadline, an extension needs a reason.

Working together#

Talk about proofs with anyone. A proof is checked by a program, and two people who arrive at the same proof by talking have both learned what the program needs. What you submit must be typed by you, and the write-ups you submit must be in your words. The verifier project is the exception: its code is written by you alone, in whatever language you choose. You may read anything, including the source of other verifiers, as its page says; what you may not do is submit code you did not write.

Tools#

Any editor, any operating system, any proof assistant. The course teaches mmj2 and the labs assume it, but a proof that verifies is a proof. Language models and other generators may be used for the lab proofs and the definition exercise; say so in one line when you submit. They may not be used to write the verifier project’s code.

What you may do with what you produce#

The databases the course works in are public domain: the Metamath project’s copyright page says its databases “are waived of all rights, including copyright, according to the CC0 Public Domain Dedication”. A proof you write in a lab is yours to publish, contribute or forget. This site’s own text is licensed as the footer says.

Getting help#

The lab is the place to get unstuck. Between labs, email the tutor with the proof file attached, or the convenor for anything that is not a proof.