This repository holds some formalizations of knot theory proofs in lean.

Currently planning on:

• underlying representation of bricks/walls basic
• notion of planar isotopy equivalence basic
• notion of reidemeister move equivalence basic
• proof that brick/wall notions of equivalency are sufficient (not sure how to do this?)
• definition of tangle tangle
• tangle surgery or inductive notion of tangle equivalency
• proof of tangle invariance across notions of equivalence tangle
• definition of link link
• definition of knot link
• definition of braid braid
• definition of permutation, proof that braid is a permutation

Not quite sure about the following:

• notion of tri-colourability
• notion of alternating
• HOMFLY/Jones polynomials

References

• Prathamesh, T. V. H. (2015). Formalising Knot Theory in Isabelle/HOL. Lecture Notes in Computer Science, 438–452. doi:10.1007/978-3-319-22102-1_29 / prathamesh-t/Tangle-Isabelle