GitXplorerGitXplorer
s

leanknot

public
3 stars
2 forks
0 issues

Commits

List of commits on branch lean4.
Verified
5c50fc107c1e98978d2cd966d4c6b22348e1ee4a

thanks @kerel-fs for the link!

sshua committed 2 years ago
Unverified
ee6d22c373933893dbe79395fc8b92b07f4bf484

some work on happend and tangle lemmas

sshua committed 2 years ago
Unverified
54136b8a4f2d2cb985b3cdade8aa103bff9b97ff

split out eq cases, introduce Surgery

sshua committed 2 years ago
Unverified
4df3676fe2c24671567ac954042cf25d6a8fb00b

towards global Homotopic equivalence

sshua committed 2 years ago
Unverified
9c49be3624425b83826e8223bcec20dc9027f453

small refacs

sshua committed 2 years ago
Unverified
640a92bb8026e5f2ce524d64ec824c729a9c5614

refac: Graphs, Equivalence, braid_is_tangle

sshua committed 2 years ago

README

The README file for this repository.

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

Currently planning on:

  • [x] underlying representation of bricks/walls basic
  • [x] notion of planar isotopy equivalence basic
  • [x] notion of reidemeister move equivalence basic
  • [ ] proof that brick/wall notions of equivalency are sufficient (not sure how to do this?)
  • [x] definition of tangle tangle
  • [ ] tangle surgery or inductive notion of tangle equivalency
  • [x] proof of tangle invariance across notions of equivalence tangle
  • [x] definition of link link
  • [x] definition of knot link
  • [x] 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