CSCI1951-D

Projective Geometry via Interactive Proof Assistants

Not offered this year
Offered occasionally, last taught:

Spring 2022

We will study both real and synthetic projective geometry, leading up to showing every Desarguesian projective plane admits coordinates in some division ring. We'll do all of this using an automated proof assistant, Lean, 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: (MATH 0520, 0540 or 1530) and (CSCI 0170, 0150 or 0190) and (CSCI 0160, 0180 or 1570) or minimum score of WAIVE in 'Graduate Student PreReq'.