Projective Geometry via Interactive Proof Assistants

Course Home Page:
Offered this year?No
When Offered?Occasionally


We will study both real and synthetic projective geometry, leading up to showing every Desarguian projective plane admits coordinates in some division ring. We'll do all of this using an automated proof assistant, Isabelle, and learn something about logic and automated theorem proving at the same time.
Does not fit any pathways, but certainly fits the "Math/CS three additional courses in Math, CS, or related areas" item.
Prerequisites: one of MATH0520, MATH0540, or MATH1530; one of CSCI0170 or CSCI0150 or CSCI0190; and one of CSCI0160 or CSCI0180 or CSCI1570

CRN: None