Quadrisecants of Wild Knots Conjecture

### What is the conjecture

A **wild knot** is a knot (a closed curve homeomorphic to $S^1$ embedded in $\mathbb{R}^3$) that is not a smooth or piecewise-linear knot. Formally, it is a locally infinite knot that may have wildly oscillating behavior near certain points.

A **quadrisecant** of a knot $K \subset \mathbb{R}^3$ is a straight line that intersects $K$ at exactly four distinct points.

**Conjecture:** Every wild knot possesses infinitely many quadrisecants.

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

**Sources:**
- https://arxiv.org/abs/math/9712205, https://en.wikipedia.org/wiki/Wild_knot, https://mathworld.wolfram.com/WildKnot.html, https://en.wikipedia.org/wiki/Knot_theory, https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics#Topology

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Topological embeddings of circles in Euclidean space (manifold theory)
- Basic point-set topology and metric spaces

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of wild knots and their distinctive topological properties (local infiniteness, non-smoothness)
- Definition and theory of secant lines and their intersection multiplicities with topological curves

Rating justification: Knot theory is not substantially developed in Mathlib, and wild knots are a specialized concept in topology. Formalizing the statement would require building significant infrastructure for topological knot representations and defining quadrisecants precisely in the topological setting.

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

* ams-57

### 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)