# Cannon's conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Modulus Proof of Cannon’s Conjecture](../../preprints/A-Modulus-Proof-of-Cannons-Conjecture-September-23-2026/paper.pdf)

## Scope

Cannon's conjecture asks whether a hyperbolic group with boundary homeomorphic to the two-sphere acts geometrically on hyperbolic three-space. The formalization proves that such a group admits an isometric action on $\mathbb H^3$ that is proper and cocompact and has finite kernel. Hyperbolicity is expressed through uniformly thin geodesic triangles in a Cayley graph, and the boundary hypothesis is a homeomorphism with $S^2$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Cannon's geometric-action conclusion | [CannonGeometricAction.lean](../ComparatorChallenges/CannonGeometricAction.lean) |