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
- definition of tangle tangle
- inductive notion of tangle equivalency (will allow greater application of r-move and planar iso equiv)
- proof of tangle invariance across notions of equivalence tangle
- definition of link link
- definition of knot
- definition of braid scratch
- 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