Berge Conjecture (Dehn Surgery and Lens Spaces)

### What is the conjecture

Let $K$ be a knot in the 3-sphere $S^3$. A Dehn surgery on $K$ is a topological operation that cuts $S^3$ along a tubular neighborhood of $K$ and reglues the resulting 3-manifold by twisting. A knot $K$ is called a **Berge knot** if it is isotopic to a double primitive loop in a genus two Heegaard splitting of $S^3$, meaning it intersects an essential disk in exactly one point within both handlebodies of the splitting.

The **Berge Conjecture** states:

$$\text{If a knot } K \subset S^3 \text{ admits a non-trivial Dehn surgery producing a lens space, then } K \text{ is a Berge knot.}$$

Equivalently: the Berge knots are the only knots in $S^3$ that admit Dehn surgery to a lens space.

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

**Sources:**
- https://en.wikipedia.org/wiki/Berge_knot, https://ldtopology.wordpress.com/2007/11/19/the-berge-conjecture/, https://arxiv.org/abs/0710.0357, https://arxiv.org/abs/1701.01421, https://arxiv.org/abs/1008.1034

### 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):
- Basic 3-manifold and topology foundations (currently minimal in Mathlib)
- Homological/algebraic structures that could support homology theories

Missing pieces (exactly 2; unclear/absent from search results):
- Knot theory framework: definition of knots in $S^3$, isotopy, Dehn surgery operation, and associated manifold constructions
- Heegaard splitting theory and lens space definitions/characterization

Rating justification: Knot theory and 3-manifold topology are not substantially developed in Mathlib. Formalizing the Berge Conjecture requires building significant new infrastructure including knot types, surgery operations, and geometric properties of Heegaard splittings. The rating reflects the substantial foundational work needed to state the conjecture, not just prove it.

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

* ams-57
* ams-55
* ams-54

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

Start by reading the conjecture statement and the listed sources, then assess the missing knot theory, 3-manifold, Dehn surgery, lens space, and Heegaard splitting foundations described in the issue. Done would require adding the conjecture to the Lean repository, but the issue names no files, tests, or existing entry point and notes that substantial infrastructure is absent.

Written by the indexing model from the issue text.