CSCI1951-Y

Using an Interactive Proof Assistant to do Mathematics

Fall 2025

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.