Room 327

Formalizing Knot Theory in Isabelle/HOL

T V H Prathamesh

IMSc

Knot theory refers to a study of mathematical objects which are derived from the intuitive notion of a knotted loop of rope. Isabelle is an interactive proof assistant in which formalized proofs
can be partly automated and checked. In this talk, we describe formalization of some topics in knot theory in Higher Order Logic (HOL). The formalization was carried out in the interactive proof assistant, Isabelle. The concepts that were formalized include definitions of tangles, links, framed links and various forms of equivalences between them along with the formalization of Bracket Polynomial, an invariant of framed links.
I shall describe the formalization and the challenges that I encountered, in some detail, in this talk.