Projective Geometry via Interactive Proof Assistants
|Offered this year?||No|
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