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
- 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