### Abstract

This work contains a formalization of some topics in knot theory. The concepts that were formalized include definitions of tangles, links, framed links and link/tangle equivalence. The formalization is based on a formulation of links in terms of tangles. We further construct and prove the invariance of the Bracket polynomial. Bracket polynomial is an invariant of framed links closely linked to the Jones polynomial. This is perhaps the first attempt to formalize any aspect of knot theory in an interactive proof assistant.

### License

BSD License

### Topics

- Mathematics/Topology

### Session Knot_Theory

- Preliminaries
- Tangles
- Tangle_Algebra
- Tangle_Relation
- Tangle_Moves
- Link_Algebra
- Example
- Kauffman_Matrix
- Computations
- Linkrel_Kauffman
- Kauffman_Invariance
- Knot_Theory

### Depends on

- Tensor Product of Matrices

## Cite

×

Knot_Theory-AFP

    @article{Knot_Theory-AFP,
      author  = {T.V.H. Prathamesh},
      title   = {Knot Theory},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Knot_Theory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jan 20, 2016 : Isabelle2015