CSCI 1951Y: Using an Interactive Proof Assistant to Do Mathematics

Welcome

Welcome to the course website for the Fall 2025 edition of CSCI1951Y at Brown University! Here is some basic information about the course:

Professor: John F. Hughes, CIT 365

Head TA: Robert Shlyakhtenko

Class Schedule: MWF 2pm-2:50pm in CIT 101

Prof. Hughes' Office Hours: W 3-4:30pm, Th 4:30-5:30pm, CIT 365.

Robert's Office Hours: T 7-8pm, CIT 241; Th 4-5pm, CIT 165.

Course Description

Proof assistants are software tools based on logic. They are typically used in both mathematics and computer science to verify proofs of theorems (in mathematics) or algorithm correctness (in CS). Beginning texts often emphasize mathematical applications focused on logic, while typical undergraduate mathematics education does not. The corpora of mathematics results for many proof assistants are heavily slanted towards real analysis and abstract algebra, but have limited depth in topology and geometry. Students will learn to use the Isabelle proof assistant to initially do some proofs covering introductory material in a Calculus book, and then move on to study both real and synthetic projective geometry, leading up to showing every Desarguesian projective plane admits coordinates in some division ring. They'll also complete final projects in some geometry-related topic.

Syllabus & Course Access Links

The syllabus can be accessed here. The EdStem page is located here.

We will use Zoom to facilitate lecture recordings and to allow students to present their work in class conveniently. The Zoom link is posted on EdStem, and lecture recordings will be uploaded to Panopto. Please note that credit for in-person attendance and participation represents a significant portion of your course grade. Attending virtually is not an acceptable substitute.

Note that grades for individual assignments will be posted on Gradescope. Please contact the course staff if you do not have access to Gradescope.

We will not be using Canvas for this class. All course information will be posted here or on EdStem.

Assignments

Some assignments have multiple parts, which are due at different times. Always read the assignment PDF/EdStem announcement itself to double-check the due date. Depending on the assignment, you may be asked to turn in the assignment via Gradescope or via a commit to the Github repository.

Assignment Due Dates
Homework 1 9/05 & 9/10
Homework 2a: Spivak0 Homework 2b: Spivak1 9/17
Homework 3: Hartshorne Chapter 1-1 (posted on EdStem) 9/24 (two submissions on Gradescope, one via Github commit)

GitHub & Recordings

Course materials are available on GitHub on the CS1951Y repository. A full list of recordings is available here.

Useful Links

  1. Isabelle download link
  2. Isabelle's Zulip chat
  3. Archive of Formal Proofs
  4. Isabelle tutorial
  5. Hartshorne: Projective Geometry (PDF)
  6. Lewis: The Art of Formal Proof (PDF)
  7. Tao: Machine assisted proof (PDF)
  8. Koutsoukou-Argyraki: First Experiences with Isabelle/HOL (PDF)
  9. Teege: Gentle Introduction to Isabelle (PDF)
  10. Nipkow: Guide to Isabelle (PDF)