oai-math-revised beta

Browse › Real and complex analysis › 071 Koebe’s circle-domain conjecture

Removable Boundaries and Rigidity of Circle Domains

OpenAI · September 23, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We prove that a circle domain with conformally removable boundary is conformally rigid, with no restriction on the number of complementary components. This establishes the removability-to-rigidity direction of the He–Schramm Conjecture.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Formalization

  • OpenAI math release, Lean scope note 071: Koebe's circle-domain conjecture (lean/docs/071.md, 2026-10-06). The release's scope note says the Lean development proves the removability-to-rigidity direction of the He–Schramm conjecture with no bound on the number of complementary components, alongside Koebe's circle-domain theorem, both linked to KoebeCircleDomains.lean. [family-level]
  • OpenAI math release, KoebeCircleDomains.lean (Comparator challenge) (openai/math, commit adc7f12). The Comparator statement file has two theorems: removability_implies_rigidity (a conformal equivalence between circle domains whose source frontier is conformally removable agrees with a Möbius map) and koebe_circle_domain. [family-level]

Possibly relevant literature (found by the agent, not checked)

  • D. Ntalampekos, M. Younsi, Conformal rigidity: progress and challenges (arXiv:2610.00560, v1 30 Sep 2026). A survey on circle-domain rigidity and conformal removability, posted shortly before the release and not in the paper's bibliography; its v1 lists the removable-implies-rigid question (Theorem 1.1 here) as open, even when the whole boundary is a Cantor set.

Digests and expositions

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026,
  author = {{OpenAI}},
  title = {{Removable Boundaries and Rigidity of Circle Domains}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/paper.pdf}{OAI:Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/071.md. The Lean statements have not been checked by people against the paper's claims.

Family 071: Koebe’s circle-domain conjecture

Resolves the existence part of Koebe's circle-domain conjecture: every domain in the Riemann sphere is conformally equivalent to a domain whose complementary components are round disks or points. It also proves that circle domains with conformally removable boundary are rigid, meaning every conformal equivalence to another circle domain is Möbius, establishing this direction of the He–Schramm conjecture.

Other papers in this family: