Please note: This PhD seminar will take place in DC 2310.
Alena Gusakov, PhD candidate
David R. Cheriton School of Computer Science
Supervisors: Professors Stephen M. Watt, Chris Godsil
Codifying mathematical theories in a proof assistant is a challenging task, of which the most difficult part is, counterintuitively, structuring definitions. This results in a steep learning curve for new users and slow progress in formalizing even undergraduate level mathematics. There are many considerations one has to make, such as level of generality, readability, and ease of use in the type system, and there are typically multiple equivalent or related definitions from which to choose. Often, a definition that is ultimately selected for formalization is settled on after a lengthy trial and error process. This process involves testing potential definitions for usability by formalizing standard theorems about them, and weeding out the definitions that are unwieldy. In this talk, we examine a few case studies of the process of creating formal mathematical definitions.