Visual Algebraic Proofs for Unknot Detection

A knot diagram looks like a two-dimensional drawing of a knotted rubberband. Proving that a given knot diagram can be untangled (that is, is a trivial knot, called an unknot) is one of the most famous problems of knot theory. For a small knot diagram, one can try to find a sequence of untangling moves explicitly, but for a larger knot diagram producing such a proof is difficult, and the produced proofs are hard to inspect and understand. Advanced approaches use algebra, with an advantage that since the proofs are algebraic, a computer can be used to produce the proofs, and, therefore, a proof can be produced even for large knot diagrams. However, such produced proofs are not easy to read and, for larger diagrams, not likely to be human readable at all. We propose a new approach combining advantages of these: the proofs are algebraic and can be produced by a computer, whilst each part of the proof can be represented as a reasonably small knot-like diagram (a new representation as a labeled tangle diagram), which can be easily inspected by a human for the purposes of checking the proof and finding out interesting facts about the knot diagram.