7CCSACTP: Computer-Assisted Theorem Proving
Module Leader: Mohammad Abdulaziz
Interactive Theorem Prover: Isabelle/HOL

Isabelle/HOL Logo

Module Overview:
This module introduces students to the state-of-the-art in computer-assisted mathematical theorem proving using the Isabelle/HOL interactive theorem prover (ITP). The curriculum progresses from logical foundations and functional programming, to the formal verification of software and mathematical theories, through to modern artificial intelligence and machine learning methods for automated reasoning.

Core Module Aims:

Teaching Format:
• Flipped Classroom: Pre-recorded lecture videos and reading materials prepare students for interactive Large Group Tutorials (LGT) and Small Group Tutorials (SGT). All lecture and demonstration videos include synchronized Closed Captions (CC) and subtitle downloads (.vtt / .srt).

Textbooks & Obligatory Reading Material (Freely Available Online):
• Functional Data Structures and Algorithms: Tobias Nipkow, Mohammad Abdulaziz et al. — fdsa-book.net
• Concrete Semantics: Tobias Nipkow & Gerwin Klein — concrete-semantics.org
• Isabelle/HOL Tutorial: Tobias Nipkow, Lawrence C. Paulson, & Markus Wenzel — isabelle.in.tum.de (PDF)

Assessment Structure (50% Coursework / 50% Exam):
• 50% Coursework: Individual formal proof project released on Friday, 30 October 2026 (Week 5) and due on Thursday, 10 December 2026, 4:00 PM (Week 10). Deliverables include: (1) Informal mathematical proof writeup (up to 2 pages), (2) Design decisions report (up to 2 pages), (3) Mechanised proof theory file (.thy), and (4) AI conversation transcript export.
• 50% Exam: Paper-based written final examination in January 2027 (Examination Period 1).

Note on Practice & Demonstration Videos:
Please note that the demonstration and practice videos are not examinable in the final written examination. They are provided strictly as a practical primer to help you become comfortable with Isabelle/HOL, navigate the interface, and complete the coursework formalisation project. The final written exam assesses theoretical foundations, formal semantics, and logical reasoning covered in the core lecture materials and readings.

Demo theory files are intentionally not provided. You are meant to construct each demo theory yourself in Isabelle while following the practice and demonstration videos, pausing and typing along as you go. Building the proofs step by step is how you learn to use Isabelle.

Week 1 | Week 2 | Week 3 | Week 4 | Week 5 | Week 6 | Week 7 | Week 8 | Week 9 | Week 10

Week 1: Foundations of Computer-Assisted Theorem Proving

Week 2: Mathematical Induction & Case Analysis

Week 3: Lists, Structural Induction & Proof Automation

Week 4: Datatypes, Primitive Recursion & Trees

Week 5: AI-Assisted Theorem Proving & Agentic LLMs

Week 6: Proving Basic Algorithms Correct — Sorting & Locales

Week 7: Proving Data Structures Correct — 2-3 Trees

Week 8: Proving Graph Algorithms Correct — Depth-First Search (DFS)

Week 9: Proving Correctness & Loop Invariants

Week 10: Verifying Real-World Programs — AutoCorres2

7CCSACTP Computer-Assisted Theorem Proving — Mohammad Abdulaziz