Unknotting Problem

### What is the conjecture

A knot is a smooth embedding of the circle $S^1$ into three-dimensional Euclidean space $\mathbb{R}^3$. Two knots are equivalent if one can be continuously deformed into the other through ambient isotopy. The unknot is the trivial knot (the standard embedding of $S^1$ into $\mathbb{R}^3$).

The **unknotting problem** asks: Does there exist a finite algorithm that can decide, given any knot diagram (or equivalent representation), whether the represented knot is equivalent to the unknot?

Related is also the decision problem of determining if a knot has unknotting number 1. It is open if this decision problem is decidable and if it has a polynomial time algorithm . See here: https://epoch.ai/frontiermath/open-problems/unknotting-number

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Unknotting_problem | https://en.wikipedia.org/wiki/Knot_theory | Hass, Joel; Lagarias, Jeffrey C.; Pippenger, Nicholas (2005). "The computational complexity of knot and link problems" | Adams, Colin C. "The Knot Book: An Elementary Introduction to the Mathematical Theory of Knots"

### Prerequisites needed

Knot Theory is Missing from Mathlib.

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-02-04)

Building blocks (1-3; from search results):
- Topological embeddings and homeomorphisms (Mathlib.Topology)
- Circles and Euclidean spaces (Mathlib.Geometry)
- Basic computability/decidability concepts (Mathlib.Computability)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of knot equivalence classes under ambient isotopy
- Formal representation of knot diagrams and their relationship to spatial knots

Rating justification (1-2 sentences): Formalizing the unknotting problem requires substantial new theory development, particularly formalization of knots as equivalence classes of embeddings under ambient isotopy and knot diagrams. While basic topological and computational concepts exist in Mathlib, the specific algebraic and topological structures needed for knot theory (such as knot invariants, Reidemeister moves, and diagram equivalence) are largely absent.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-57
* ams-68

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

No repository files, tests, or entry points are named. Start by reviewing Mathlib.Topology, Mathlib.Geometry, and Mathlib.Computability against the stated missing definitions of ambient-isotopy knot equivalence and knot diagrams; done would mean adding the unknotting conjecture in the repository.

Written by the indexing model from the issue text.