Rigidity of circle domains with removable boundary
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
If every sphere homeomorphism conformal off the boundary of a circle domain D is a Mobius map, must every conformal bijection from D to another circle domain be the restriction of a Mobius map?Short English statement
If every sphere homeomorphism conformal off the boundary of a circle domain D is a Mobius map, must every conformal bijection from D to another circle domain be the restriction of a Mobius map?Sources
- S1 Original question source or mathematical context. https://www.math.stonybrook.edu/~bishop/classes/math536.S24/He_Schramm_1993.pdf.
- S2 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2953
Rigidity from removability: The primary statement says: A circle domain with conformally removable boundary has the property that every conformal bijection onto another circle domain is a Mobius restriction. The target retains these quantified objects and hypotheses, so its positive assertion is covered.
With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.
Rigidity of circle domains with removable boundary
OpenAI's claim
Rigidity from removability: The paper claims that a conformal map between circle domains must be a restriction of a Möbius map whenever the source boundary is conformally removable. No finiteness condition is placed on the collection of holes.Mathematical statement of the claimed result
Mathematical claim 1.
Let $\Omega,\Omega^\prime\subset\widehat{\mathbb C}$ be circle domains, meaning that every complementary component is a round disk or a point. Suppose that $\partial\Omega$ is conformally removable: every sphere homeomorphism conformal off $\partial\Omega$ is a Möbius transformation. Every conformal bijection $f:\Omega\to\Omega^\prime$ then has the form $f=M|_\Omega$ for a Möbius map $M$.Outline of the argument
Rigidity from removability: Scalar tests are carried into circle-domain models on successively larger compact regions. A Beltrami-based conductivity variation constructs low-energy coordinate barriers, which force any remaining omitted component to shrink to a point. The resulting scalar extension theorem and masks around disk components give a flux comparison; equality in the associated area estimates determines the conformal map.Formal verification
Family 071 describes Lean coverage for the universal circle-domain representative and the Möbius rigidity implication under removable source boundary.Rigidity from removability: The manuscript links KoebeCircleDomains.lean.
The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, Removable Boundaries and Rigidity of Circle Domains, 2026-09-23; citation key
OAI:Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 071: Lean scope.
- Comparator KoebeCircleDomains.json.
- Comparator KoebeCircleDomains.lean.
- OpenAI catalogue entry.