google-deepmind / google-deepmind/formal-conjectures

Volume Conjecture

Open
#2,190 0 comments 0 reactions 0 assignees View on GitHub
ams-55: Algebraic topology ams-57: Manifolds and cell complexes ams-81: Quantum theory needs-prerequisites new conjecture wikipedia
Dominant language
Lean
Stars
1.3k
Forks
485
Avg merge
1d 20h
Merged PRs (30d)
327

Description

### What is the conjecture

For a hyperbolic knot $K$ in the 3-sphere $S^3$, the asymptotic growth rate of the $N$-colored Jones polynomial at primitive $N$-th roots of unity equals the hyperbolic volume of the knot complement:

$$\lim_{N \to \infty} \frac{2\pi \log|J_N(K; e^{2\pi i/N})|}{N} = \text{Vol}(S^3 \setminus K)$$

Here, $J_N(K; q)$ is the $N$-colored Jones polynomial (a quantum invariant derived from the $N$-dimensional representation of the quantum group $U_q(\mathfrak{sl}_2)$), and $\text{Vol}(S^3 \setminus K)$ is the hyperbolic volume of the knot complement, which exists when $K$ is a hyperbolic knot (i.e., when its complement admits a complete hyperbolic metric of constant curvature $-1$). For non-hyperbolic knots, the conjecture can be stated using simplicial volume. The conjecture was originally formulated by Kashaev (1997) and restated in modern form by Murakami and Murakami (2001) using the colored Jones polynomial.

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

**Sources:**
- https://en.wikipedia.org/wiki/Volume_conjecture, https://ncatlab.org/nlab/show/volume+conjecture, Murakami & Murakami (2001). The colored Jones polynomials and the simplicial volume of a knot. *Acta Mathematica* 186: 85–104, Murakami et al. (2002). Kashaev's conjecture and the Chern-Simons invariants of knots and links. *Experimental Mathematics* 11(3): 427–435, https://arxiv.org/abs/1002.0126

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Real and complex limits, logarithms, absolute value (in Mathlib.Analysis)
- Complex roots of unity (in Mathlib.Data.Complex.Exponential)

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of knot theory: definition of knots, links, and invariants (knot complements, Reidemeister moves, knot type equivalence)
- Colored Jones polynomial: quantum group representations, the $N$-colored Jones polynomial from $U_q(\mathfrak{sl}_2)$ theory, and hyperbolic volume of 3-manifolds

Rating justification: The statement requires building substantial infrastructure for knot theory and quantum topology from scratch. While basic analysis and complex number operations exist in Mathlib, there is no formalized knot theory library, no quantum group representation theory, and no hyperbolic geometry framework for 3-manifolds. Even stating the conjecture requires formalizing the entire framework of knot invariants and hyperbolic volume.

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

* ams-57
* ams-55
* ams-81

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

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.