| February 6 | introduction, Mizar: 1.1-1.2 | QED manifesto, Mizar tutorial | |
| exercise Mizar | exercise | ||
| February 16 | Mizar: 1.3 | ||
| March 2 | Mizar: 1.4-1.5 | ||
| March 9 | Mizar: 1.6-1.8 | ||
| March 23 | Mizar: 2.1-2.3 | ||
| March 26 | checkpoint Mizar | ||
| March 30 | Mizar: "by" | "by" paper | |
| April 13 | Systems: overview | seventeen provers | |
| exercise HOL | exercise | ||
| April 20 | HOL: logic | HOL manual, HOL logic chapter | |
| April 23 | selecting system | ||
| April 27 | HOL: kernel | hol.ml, type.ml, term.ml, thm.ml, bool.ml | |
| May 7 | deadline Mizar | ||
| May 11 | HOL: goals, tactics | HOL reference, tactics.ml | |
| May 25 | HOL: conversions, rewriting | equal.ml, drule.ml, simp.ml | |
| June 1 | HOL: decision procedures | model elimination | |
| June 4 | checkpoint HOL | ||
| June 13 | presentations: | (one time: HG00.068) | |
| Systems: Isabelle/Isar | Ronny Wichers Schreur | ||
| Systems: Otter/Ivy/EQP/Prover9 | Freek Verbeek | ||
| June 15 | presentations: | ||
| Systems: minlog | Venanzio Capretta | ||
| Systems: Epigram | Eelis van der Weegen | ||
| June 22 | presentations: | ||
| Systems: ssreflect | Jorik Mandemaker | ||
| Systems: KIV | Arjen Hommersom | ||
| July 2 | deadline HOL |