Geometry & Topology

Motivation

A finitely generated group is (word-)hyperbolic if the geodesic triangles in its Cayley graph are uniformly thin, as in the hyperbolic plane. Such a group has a boundary at infinity $\partial G$, a compact space of asymptotic directions. The fundamental group of a closed hyperbolic 3-manifold is hyperbolic with boundary the 2-sphere. Cannon's conjecture asks for the converse: if a hyperbolic group has boundary homeomorphic to $S^2$, does it act geometrically on hyperbolic three-space $\mathbb H^3$? An affirmative answer characterizes, purely in terms of coarse geometry, which groups arise from closed hyperbolic 3-manifolds; it is one of the central problems of geometric group theory and is closely tied to the geometrization program for 3-manifolds.

Timeline

• 1981, 1980. Sullivan and Tukia show that groups of uniformly quasiconformal maps of the sphere are conjugate to Möbius groups (Sullivan, Stony Brook 1978 proceedings; Tukia, doi:10.5186/aasfm.1980.0530).
• 1989. Pansu introduces conformal dimension of boundaries (doi:10.5186/aasfm.1989.1424).
• 1994. Cannon's combinatorial Riemann mapping theorem recovers quasiconformal coordinates from discrete moduli (doi:10.1007/BF02398434).
• 1998. Cannon and Swenson state the group-boundary conjecture and relate geometric actions to conformality of boundary coverings (doi:10.1090/S0002-9947-98-02107-2).
• 1999. Cannon, Floyd and Parry reduce the problem to bounded discrete moduli of annuli at small scales (Ann. Acad. Sci. Fenn. Math., 1999).
• 2002, 2005. Bonk and Kleiner develop quasisymmetric uniformization of metric spheres and prove the conjecture when the Ahlfors-regular conformal dimension is attained (doi:10.1007/s00222-002-0233-z, doi:10.2140/gt.2005.9.219).
• 2012–2013. Kahn–Marković, Bergeron–Wise, Agol and Marković connect surface subgroups, cubulation and Kleinian realizations (doi:10.4007/annals.2012.175.3.4, doi:10.4171/DM/421, doi:10.1007/s00039-013-0228-5). Bourdon and Kleiner give a combinatorial-modulus criterion for uniformization (doi:10.4171/GGD/177).
• 2015. Haïssinsky proves a virtual Kleinian criterion for cubulated hyperbolic groups with planar boundary (doi:10.1007/s00222-014-0552-x).
• 2026. Groves, Haïssinsky, Manning, Osajda, Sisto and Walsh reduce the residually finite case to the Toral Relative Cannon conjecture (arXiv:2406.14667).

The source of this mission, an OpenAI preprint dated September 23, 2026, follows the analytic route and proves the conjecture.

Setting

Let $G$ be a group with a finite symmetric generating set $S$ and Cayley graph $\Gamma(G,S)$ with graph distance $d$. $G$ is hyperbolic if there is $\delta$ such that every point on a side of a geodesic triangle lies within $d\le\delta$ of the union of the other two sides. A geodesic ray based at $1$ is a sequence $r_0=1,r_1,\dots$ with $d(r_i,r_j)=|i-j|$; two rays are equivalent if $d(r_n,s_n)$ stays bounded. The boundary $\partial G$ is the set of equivalence classes with the quotient of the topology of pointwise convergence.

$\mathbb H^3$ is the upper half-space $\{x\in\mathbb R^3: x_3>0\}$ with distance $\operatorname{arcosh}\bigl(1+|x-y|^2/(2x_3y_3)\bigr)$, and $\operatorname{Isom}(\mathbb H^3)$ is its full isometry group, including orientation-reversing isometries. A homomorphism $\rho:G\to\operatorname{Isom}(\mathbb H^3)$ gives a proper action if $\{g:\rho(g)K\cap K\ne\varnothing\}$ is finite for every compact $K$, and a cocompact action if translates of one compact set cover $\mathbb H^3$.

Formalization targets

Goal: Theorem 1.1

The Lean statement OAI.CannonRelease.cannon is open on the platform.

Significance

The theorem identifies hyperbolic groups with 2-sphere boundary, up to finite kernels, with uniform lattices in $\operatorname{Isom}(\mathbb H^3)$. For torsion-free $G$, the quotient $\mathbb H^3/G$ is a closed hyperbolic 3-manifold, possibly nonorientable (Corollary 8.1), and the work of Kahn–Marković, Bergeron–Wise and Agol then gives virtual structure results (Corollary 8.2). It also settles the hypotheses of the reductions of Marković and of Groves et al. in full generality.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would require formal infrastructure for hyperbolic groups and their boundaries, quasiconformal analysis and combinatorial modulus, very little of which is currently in Mathlib.

Difficulty

By the Cannon–Floyd–Parry and Bourdon–Kleiner criteria, the theorem reduces to a uniform upper bound on the combinatorial 2-modulus of curve families at all scales of the boundary. The bound is easy to state but there is no a priori reason why moduli of coverings of a topological sphere should stay bounded; Bonk–Kleiner needed the extra hypothesis that the conformal dimension is attained. A proof must extract analytic control (a nonconstant limit function with controlled oscillation) from a hypothetical sequence of coverings with unbounded modulus and contradict it using only hyperbolicity and the topology of the boundary.

Formalization scope

• CayleyData G is a finite symmetric generating set with connected SimpleGraph.mulCayley; ThinTriangles asks for one natural number $\delta$ working for all geodesic triangles given as walks of length equal to graph distance.
• Rays are ℕ → G with r 0 = 1 and dist (r i) (r j) = |i-j|; the boundary is the quotient by bounded synchronous distance. $G$ carries the discrete topology, rays the subspace product topology, and the boundary the quotient topology, which coincides with the visual topology for hyperbolic groups.
• $S^2$ is the unit sphere in EuclideanSpace ℝ (Fin 3); $\mathbb H^3$ is the upper half-space with the explicit arcosh distance and subspace topology; isometries are self-homeomorphisms preserving that distance.
• The kernel is only required to be finite, and orientation-reversing elements are allowed, matching the paper.

A complete development needs Gromov hyperbolic groups and visual metrics, approximately self-similar spheres, combinatorial modulus and the Bonk–Kleiner/Bourdon–Kleiner uniformization criterion, and the Sullivan–Tukia straightening of uniformly quasiconformal groups. Contributions formalizing Proposition 2.6 (from a round boundary action to a geometric action on $\mathbb H^3$) or Theorem 2.5 (the uniformization criterion) are welcome.

Selected references

• OpenAI, A Modulus Proof of Cannon's Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Modulus-Proof-of-Cannons-Conjecture-September-23-2026/paper.pdf
• J. W. Cannon, The combinatorial Riemann mapping theorem, Acta Math., 1994. https://doi.org/10.1007/BF02398434
• J. W. Cannon, E. L. Swenson, Recognizing constant curvature discrete groups in dimension 3, Trans. Amer. Math. Soc., 1998. https://doi.org/10.1090/S0002-9947-98-02107-2
• J. W. Cannon, W. J. Floyd, W. R. Parry, Sufficiently rich families of planar rings, Ann. Acad. Sci. Fenn. Math., 1999. https://www.acadsci.fi/mathematica/Vol24/cannon.pdf
• M. Bonk, B. Kleiner, Quasisymmetric parametrizations of two-dimensional metric spheres, Invent. Math., 2002. https://doi.org/10.1007/s00222-002-0233-z
• M. Bonk, B. Kleiner, Conformal dimension and Gromov hyperbolic groups with 2-sphere boundary, Geom. Topol., 2005. https://doi.org/10.2140/gt.2005.9.219
• M. Bourdon, B. Kleiner, Combinatorial modulus, the combinatorial Loewner property, and Coxeter groups, Groups Geom. Dyn., 2013. https://doi.org/10.4171/GGD/177
• V. Marković, Criterion for Cannon's conjecture, Geom. Funct. Anal., 2013. https://doi.org/10.1007/s00039-013-0228-5
• P. Haïssinsky, Hyperbolic groups with planar boundaries, Invent. Math., 2015. https://doi.org/10.1007/s00222-014-0552-x
• D. Groves, P. Haïssinsky, J. F. Manning, D. Osajda, A. Sisto, G. S. Walsh, Drilling hyperbolic groups, preprint, 2026. https://arxiv.org/abs/2406.14667

Motivation

The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.

Timeline

• 1908. Koebe poses the problem (Nachr. Ges. Wiss. Göttingen, 1908).
• 1920. Koebe's treatment of the finitely connected case (doi:10.1007/BF01199400).
• 1993. He and Schramm prove the conjecture for countably connected domains (doi:10.2307/2946541).
• 1995. Schramm introduces transboundary extremal length and treats domains bounded by points and $K$-quasicircles (doi:10.1007/BF02788827).
• 2025. Rajala shows that arbitrary interior exhaustions can fail to have circle-domain limits and proves an exhaustion refinement theorem for countably connected domains (doi:10.1353/ajm.2025.a966291); Ntalampekos and Rajala study exhaustions of circle domains (arXiv:2312.06840).
• 2026. Esmayli and Rajala prove uniformization for cospread domains and under a quasitripod condition (arXiv:2401.08485); Karafyllia and Ntalampekos treat spherical Gromov-hyperbolic domains (arXiv:2405.13782). Ntalampekos surveys the area (arXiv:2603.15098).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.

Setting

The Riemann sphere is $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$, with local coordinate $z$ near finite points and $1/z$ near $\infty$. A domain is a nonempty connected open subset. A map $f$ is conformal at $p$ if it is continuous at $p$ and, in these coordinates, complex differentiable at $p$ with nonzero derivative. A conformal equivalence $f:U\to V$ is a bijection that is conformal at every point of $U$ and whose inverse is conformal at every point of $V$.

A closed round disk in $\widehat{\mathbb C}$ is the image of the closed unit disk under a Möbius transformation $z\mapsto (az+b)/(cz+d)$, $ad-bc\ne0$; these are closed Euclidean disks, closed half-planes together with $\infty$, and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.

Formalization targets

Goal: Theorem 1.1 (circle-domain uniformization)

Lean: OAI.Problem047.koebe_circle_domain, open on the platform.

Significance

The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in $\partial_\infty\mathbb H^3$ whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.

The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.

Difficulty

The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.

Formalization scope

• Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.
• IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of $f$ in the charts chart p, chart (f p) (identity coordinate at finite points, $z\mapsto1/z$ at $\infty$).
• IsConformalEquivalence f U V: $f$ conformal on $U$, MapsTo f U V, and a conformal g on $V$ with MapsTo g V U that is a two-sided inverse.
• IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).
• The goal quantifies over all open connected U; there is no countability or regularity assumption on the complement.

A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.

Selected references

• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf
• P. Koebe, Über die Uniformisierung beliebiger analytischer Kurven (Dritte Mitteilung), Nachr. Ges. Wiss. Göttingen, 1908.
• P. Koebe, Abhandlungen zur Theorie der konformen Abbildung VI, Math. Z., 1920. https://doi.org/10.1007/BF01199400
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• O. Schramm, Transboundary extremal length, J. Analyse Math., 1995. https://doi.org/10.1007/BF02788827
• K. Rajala, Uniformization of planar domains by exhaustion, Amer. J. Math., 2025. https://doi.org/10.1353/ajm.2025.a966291
• D. Ntalampekos, K. Rajala, Exhaustions of circle domains, IMRN, 2025. https://doi.org/10.1093/imrn/rnaf296
• B. Esmayli, K. Rajala, Conformal uniformization of domains bounded by quasitripods, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0035
• C. Karafyllia, D. Ntalampekos, Uniformization of Gromov hyperbolic domains by circle domains, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0076
• D. Ntalampekos, Uniformization problems in the plane: A survey, preprint, 2026. https://arxiv.org/abs/2603.15098

Motivation

A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.

Timeline

• 1993. He and Schramm prove uniformization and rigidity for countably connected circle domains (doi:10.2307/2946541).
• 1994. He and Schramm prove rigidity when the boundary has $\sigma$-finite linear measure, and conjecture that rigidity is equivalent to conformal removability of the boundary (doi:10.1007/BF01231761).
• 2000. Jones and Smirnov relate removability for continuous Sobolev functions to quasiconformal removability (doi:10.1007/BF02384320).
• 2016. Younsi proves that conformal rigidity is equivalent to quasiconformal rigidity and studies the removability formulations (doi:10.1016/j.aim.2016.08.039).
• 2020. Ntalampekos and Younsi prove rigidity under square integrability of the quasihyperbolic distance, covering Hölder and John circle domains (doi:10.1007/s00222-019-00921-1).
• 2023–2024. Ntalampekos proves rigidity when point components are countably negligible for extremal distance (CNED) and continuous Sobolev extension across closed CNED sets (doi:10.1090/tran/8923, doi:10.1007/s00029-024-00951-5).
• 2025. Rajala constructs a rigid circle domain with non-removable boundary, so rigidity does not imply removability (doi:10.1112/plms.70081).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.

Setting

The Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$ has local coordinates $z$ and $1/z$. A map is conformal at $p$ if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence $f:\Omega\to\Omega'$ is a bijection, conformal on $\Omega$, with conformal inverse. A Möbius transformation is $z\mapsto(az+b)/(cz+d)$ with $ad-bc\neq0$. A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.

A compact $E\subset\widehat{\mathbb C}$ is conformally removable if every orientation-preserving homeomorphism of $\widehat{\mathbb C}$ that is conformal on $\widehat{\mathbb C}\setminus E$ is Möbius. A circle domain $\Omega$ is conformally rigid if every conformal equivalence from $\Omega$ onto another circle domain is the restriction of a Möbius transformation.

Formalization targets

Goal: Theorem 1.1

Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of $f$ is assumed.

Significance

Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions ($\sigma$-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending $f$ to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of $\Omega$ may correspond to a disk component of $\Omega'$ and vice versa, so the coordinates of $f$ need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.

Formalization scope

• Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts $z$ and $1/z$ with HasDerivAt and a nonzero derivative.
• IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.
• IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.
• The boundary is frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.
• The shared definitions are those of the Koebe circle-domain mission of the same family.

A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.

Selected references

• OpenAI, Removable Boundaries and Rigidity of Circle Domains, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/paper.pdf
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• Z.-X. He, O. Schramm, Rigidity of circle domains whose boundary has σ-finite linear measure, Invent. Math., 1994. https://doi.org/10.1007/BF01231761
• M. Younsi, Removability, rigidity of circle domains and Koebe's conjecture, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2016.08.039
• D. Ntalampekos, M. Younsi, Rigidity theorems for circle domains, Invent. Math., 2020. https://doi.org/10.1007/s00222-019-00921-1
• D. Ntalampekos, Rigidity and continuous extension for conformal maps of circle domains, Trans. Amer. Math. Soc., 2023. https://doi.org/10.1090/tran/8923
• D. Ntalampekos, CNED sets: countably negligible for extremal distances, Selecta Math., 2024. https://doi.org/10.1007/s00029-024-00951-5
• P. W. Jones, S. K. Smirnov, Removability theorems for Sobolev functions and quasiconformal maps, Ark. Mat., 2000. https://doi.org/10.1007/BF02384320
• K. Rajala, Rigid circle domains with non-removable boundaries, Proc. Lond. Math. Soc., 2025. https://doi.org/10.1112/plms.70081
• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026.

Motivation

A global surface of section reduces a flow on a closed 3-manifold to an area-preserving map of a surface. It is a compact embedded surface whose boundary consists of periodic orbits, whose interior is transverse to the flow, and which every other trajectory hits infinitely often in forward and backward time. Poincaré introduced the idea for the restricted three-body problem. Once a section is a disk, results on area-preserving disk maps (Brouwer, Franks) give periodic orbits and other structure for the whole flow.

For Hamiltonian flows on star-shaped energy surfaces in $\mathbb{R}^4$, equivalently Reeb flows on the tight 3-sphere, it is natural to ask which periodic orbits bound such a disk. Hryniewicz's criterion answers this for dynamically convex flows, with no genericity assumption. The answer is purely topological: a periodic orbit bounds a disk-like global section exactly when it is unknotted with self-linking number $-1$. The criterion is used in celestial mechanics: Joung and van Koert apply it to validated periodic orbits of the restricted three-body problem (arXiv:2407.19159).

Timeline.

• 1998. Hofer, Wysocki and Zehnder prove that every dynamically convex contact form on $S^3$ has some periodic orbit $P_0$, with Conley–Zehnder index $3$, that bounds a disk-like global section. That disk is a page of an open book adapted to the flow. Strictly convex energy surfaces in $\mathbb{R}^4$ are dynamically convex (Ann. of Math. 148).
• 2008/2012. Hryniewicz proves the "unknotted, self-linking $-1$" characterization in the non-degenerate case (arXiv:0812.4076).
• 2010/2011. Hryniewicz and Salomão treat non-degenerate tight contact forms on $S^3$. Two extra conditions appear there: $\mu_{CZ}\ge 3$, and linking with every orbit of index $2$ (arXiv:1006.0049).
• 2011/2014. Hryniewicz removes non-degeneracy for dynamically convex forms (arXiv:1105.2077, Theorem 1.7). In the same paper, Theorem 1.8 shows that any orbit coming from a fixed point of the first-return map of a disk-like section is again such a binding.
• 2012. Albers, Fish, Frauenfelder, Hofer and van Koert use this circle of ideas to get disk-like sections in the planar circular restricted three-body problem (arXiv:1103.3881).

Setting

Use coordinates $x=(q_1,p_1,q_2,p_2)$ on $\mathbb{R}^4$, the Liouville form $\lambda_0=\tfrac12\sum_j (q_j\,dp_j-p_j\,dq_j)$ and the symplectic form $\omega_0=d\lambda_0=\sum_j dq_j\wedge dp_j$.

Let $H:\mathbb{R}^4\to\mathbb{R}$ be smooth and set $S=H^{-1}(1)$. Assume that every ray from the origin meets $S$ exactly once, and that it crosses $S$ transversally:

Then $S$ is a strictly star-shaped hypersurface diffeomorphic to $S^3$. Every contact form on $S^3$ that matters below arises this way, up to diffeomorphism (see Formalization scope).

The Hamiltonian vector field $X_H$ is defined by $\iota_{X_H}\omega_0=-dH$. With this sign, $\lambda_0(X_H)=\tfrac12\,dH(x)\,x>0$ on $S$. So $X_H|_S$ is a positive multiple of the Reeb vector field of the contact form $\lambda_0|_S$, and its orbits are the Reeb orbits reparametrized. A periodic orbit $P=(x,T)$ is a solution with $x(T)=x(0)$ and $T>0$. It is prime when $T$ is its least positive period. The contact structure is $\xi=\ker\lambda_0|_S$.

• Conley–Zehnder index. Fix the global frame of $\xi$ given by the quaternionic rotations of $\nabla H$. Along $P$, the linearized flow restricted to $\xi$ is a path $\varphi:[0,1]\to Sp(1)$ with $\varphi(0)=I$. The winding interval $I(\varphi)$ collects the total rotations of all nonzero vectors, measured in turns. Then $\mu_{CZ}(P)$ is the lower semicontinuous index of Hryniewicz's §2.1.1. In particular,

that is, every nonzero transverse vector turns by more than one full turn.

• Dynamical convexity. The flow is dynamically convex if $\mu_{CZ}(P)\ge 3$ for every periodic orbit $P$ in $S$, prime or multiply covered.
• Disk-like global surface of section. A smoothly embedded closed disk $D\subset S$ such that $\partial D=x(\mathbb{R})$ for a periodic orbit $P$, $X_H$ is transverse to $D\setminus\partial D$, and every trajectory not contained in $\partial D$ meets $D$ at arbitrarily large positive and negative times. Then $P$ bounds $D$.
• Unknotted. $P$ is unknotted if $x(\mathbb{R})$ is the boundary of some smoothly embedded closed disk in $S$.
• Self-linking number. Push $x$ off itself along the global frame of $\xi$ to a disjoint loop $x'$. Then

the linking number in $S\cong S^3$, with $S$ oriented as the boundary of the star-shaped domain it bounds. This agrees with Hryniewicz's Definition 1.5, which uses a section of $\xi$ over a spanning disk.

Formalization targets

Goal: Hryniewicz's criterion (Theorem 1.7, first sentence)

For every dynamically convex strictly star-shaped $S$ and every prime periodic orbit $\bar P$:

The statement fixes no constants and no non-degeneracy, and it covers every dynamically convex star-shaped surface.

Stronger: adapted open book (Theorem 1.7, second sentence)

If $\bar P$ is unknotted with $\operatorname{sl}(\bar P)=-1$, then $S\setminus \bar x(\mathbb{R})$ fibres smoothly over $\mathbb{R}/\mathbb{Z}$. Every fibre is the interior of a disk-like global surface of section whose oriented boundary is $\bar P$.

Further: new bindings from fixed points (Theorem 1.8)

Let $D_0$ be any disk-like global section. Every periodic orbit through a fixed point of the first-return map of $D_0\setminus\partial D_0$ is unknotted, has self-linking number $-1$, and so bounds the page of an adapted open book.

Significance

The result. The criterion turns a dynamical question into a topological check. It does not depend on whether the orbit is degenerate, and degenerate orbits are what one meets at bifurcations and on symmetric levels. Every periodic orbit in a strictly convex energy surface that is unknotted with $\operatorname{sl}=-1$ is a binding, so the flow is organised by many open books at once. Theorem 1.8 makes this concrete: the Hamiltonian flow twists around two different bindings, $\partial D_0$ and $\partial D_1$. In applications, numerically validated orbits become analytic global sections without a separate non-degeneracy check (Joung–van Koert, Theorems 1.2 and 1.5).

Formalizing it. The theorem is proved, in a 50-page paper that relies on Hofer–Wysocki–Zehnder's theory of pseudo-holomorphic curves in symplectizations. It has no machine-checked proof. Mathlib has no Conley–Zehnder index, no self-linking number, no linking number of curves in $S^3$, and no global surfaces of section. A Lean statement fixes every sign and orientation convention involved: the sign of $X_H$, the orientation of $S$, which push-off defines $\operatorname{sl}$, and the index of degenerate orbits. Each of these is easy to get wrong in prose. Formal proofs of the parts that use no holomorphic curves are valuable on their own: the necessity direction, the description of the index by winding intervals, and the explicit ellipsoid examples.

Difficulty

The obvious route is to approximate the contact form by non-degenerate forms $\lambda_k\to\lambda$ that keep $\bar P$ as an orbit, and then apply the non-degenerate theorems. This fails. The $\lambda_k$ need not be dynamically convex. They can have orbits of very high action with $\mu_{CZ}=2$ that are not linked with $\bar P$, so the Hryniewicz–Salomão criterion does not apply to $\lambda_k$ (Hryniewicz, p. 4). The families of planes that would give the pages for $\lambda_k$ have to be controlled directly as $k\to\infty$, and this is not a formal limit argument.

A second obstruction is genuinely global. A disk spanning $\bar P$ and transverse to the flow in its interior is easy to produce when $\operatorname{sl}(\bar P)=-1$. Showing that every trajectory returns to it is the whole content of the theorem, and no local or perturbative argument gives it.

For the formalization, nothing in the proof of sufficiency avoids finite-energy pseudo-holomorphic planes: Fredholm theory, asymptotic analysis, bubbling-off and compactness all enter. None of this exists in Lean.

Formalization scope

• Ambient space. $\mathbb{R}^4$ is Fin 4 → ℝ with coordinates ordered $(q_1,p_1,q_2,p_2)$. $\lambda_0$, $\omega_0$ and $X_H$ are defined explicitly, with the sign conventions above.
• Energy surfaces. Star-shaped surfaces are smooth (ContDiff ℝ ⊤) functions $H$ with the ray condition and $dH(x)x>0$ on $H^{-1}(1)$. The Reeb flow of a general dynamically convex form on $S^3$ reduces to this case, up to diffeomorphism and positive time change: such a form is tight (Hofer–Wysocki–Zehnder), and every tight form on $S^3$ comes from a star-shaped hypersurface (Eliashberg 1992). That reduction is not part of the targets. Hryniewicz makes the same reduction (§3, first paragraph).
• Flow. The flow is the flow of $X_H$, not of the Reeb field. All notions in the targets are invariant under positive time change. Periodic orbits are solutions of $\dot x=X_H(x)$ on all of $\mathbb{R}$. "Prime" means the recorded period is least.
• Index. $\mu_{CZ}\ge 3$ is encoded by the winding-interval condition in the global quaternionic frame, with degenerate orbits included. Multiply covered orbits are included in dynamical convexity.
• Disks. Disks are smooth embeddings of the closed unit disk (injective, with injective differential up to the boundary). The return condition demands hits at arbitrarily large positive and negative times.
• Ruling out vacuous encodings. A version without the two-sided return condition, with a dynamical-convexity predicate that no surface satisfies, or with $\operatorname{sl}$ that is not a linking number of the push-off, proves a different theorem. The ellipsoid milestone below is a non-vacuity check on the definitions.
• Infrastructure. A complete development needs the following.
  • Reusable beyond this mission: the Conley–Zehnder index of paths in $Sp(1)$, the linking number of disjoint loops in $S^3$ (or in $\mathbb{R}^3$ after stereographic projection), and global flows of vector fields on compact level sets.
  • Specific to this proof: contact topology of spanning disks (characteristic foliations, elimination of singularities), and finite-energy planes in $\mathbb{R}\times S^3$ with their Fredholm, asymptotic and compactness theory.
• Contributions welcome. The definition layer, the index and linking-number libraries, the ellipsoid examples, Lemma 2.1, the necessity direction, Lemma 3.12, and any sub-step of the holomorphic-curve argument stated as an independent lemma.

Selected references

• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
• U. L. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931. https://arxiv.org/abs/0812.4076
• U. L. Hryniewicz, P. A. S. Salomão, On the existence of disk-like global sections for Reeb flows on the tight 3-sphere, Duke Math. J. 160 (2011), 415–465. https://arxiv.org/abs/1006.0049
• U. L. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), 791–862. https://arxiv.org/abs/1105.2077
• U. L. Hryniewicz, P. A. S. Salomão, Global surfaces of section for Reeb flows in dimension three and beyond, Proc. ICM 2018 (extended version). https://arxiv.org/abs/1712.01925
• P. Albers, J. W. Fish, U. Frauenfelder, H. Hofer, O. van Koert, Global surfaces of section in the planar restricted 3-body problem, Arch. Ration. Mech. Anal. 204 (2012), 273–284. https://arxiv.org/abs/1103.3881
• C. Joung, O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. https://arxiv.org/abs/2407.19159
• Y. Eliashberg, Contact 3-manifolds twenty years since J. Martinet's work, Ann. Inst. Fourier 42 (1992), 165–192. https://doi.org/10.5802/aif.1288

Motivation

The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound $\pi/2+2/\pi\approx2.2074$ and the upper bound $2\sqrt{2}\approx2.828$ in 1968. Joseph Gerver constructed a shape of area approximately $2.2195$ in 1992 and described four constants $A$, $B$, $\varphi$, $\theta$ satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.

Timeline: Moser poses the problem (1966); Hammersley gives the $\pi/2+2/\pi\approx2.2074$ lower bound and the $2\sqrt{2}\approx2.828$ upper bound (1968); Gerver exhibits the $2.2195$ shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).

Setting

Work in the plane $\mathbb{R}^2$. The hallway is $(-\infty,1]\times[0,1]\cup[0,1]\times(-\infty,1]$, the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set $s$ in the horizontal side together with a continuous path $m$ of plane isometries indexed by the unit interval, starting at the identity, keeping the image of $s$ inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group $E(2)$; continuity together with $m(0)=\mathrm{id}$ forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas $\mathrm{volume}(s)$ over all moving sofas. The supremum is finite, at least $11/5$, and attained.

Gerver's shape is defined from a rotation path. For constants $A$, $B$, $\varphi$, $\theta$, let $r$ be the piecewise function with breakpoints $\varphi$, $\theta$, $\pi/2-\theta$, $\pi/2-\varphi$ from Romik's Theorem 2, let $x$ and $y$ be its cosine and sine integrals, and let $p$ be the associated translation path. The sofa for those constants is the intersection over angles in $[0,\pi/2]$ of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with $0\le\varphi\le\theta\le\pi/4$ and $0\le A$, $0\le B$. The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.

Formalization targets

Goal: optimality of Gerver's sofa

For every $A$, $B$, $\varphi$, $\theta$ satisfying ABphiThetaSpec,

The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.

Supporting targets

The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.

Significance

The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure $11/5\le\mathrm{volume}\le\infty$ proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional $Q$ on caps. Without it the exact maximum remains unknown.

Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.

Difficulty

The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional $Q$ an upper bound, and $Q$ need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle $\pi/2$ are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.

Formalization scope

Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions $r$, $x$, $y$, $p$ take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value $2.2195$ instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the $11/5$ certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.

Selected references

• Jineon Baek, Optimality of Gerver's Sofa, arXiv:2411.19826, 2024. https://arxiv.org/abs/2411.19826
• Joseph L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42 (1992), 267-283.
• Dan Romik, Differential equations and exact solutions in the moving sofa problem, Experimental Mathematics 27 (2018), 316-330. https://arxiv.org/abs/1606.08111
• Dean Cureton et al., MovingSofa: Autoformalization of Baek's solution, 2026. https://github.com/deancureton/MovingSofa
• Google DeepMind, formal-conjectures, FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjectures
• Dawid Trela, GerverSofaLean v1.1.0. https://github.com/dawidmtrela-dotcom/GerverSofaLean