∑math20

Real and complex analysis · Result 071

Koebe’s circle-domain conjecture

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of Removable Boundaries and Rigidity of Circle Domains

Removable Boundaries and Rigidity of Circle Domains

OpenAI · September 23, 2026

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.

Read PDF Download Source

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}
}
First page of Koebe's Circle-Domain Conjecture

Koebe's Circle-Domain Conjecture

OpenAI · September 23, 2026

We prove that every domain in the Riemann sphere is conformally equivalent to a circle domain, resolving Koebe's circle-domain conjecture positively.

Read PDF Download Source

Cite
@misc{OAI:Koebes-Circle-Domain-Conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{Koebe's Circle-Domain Conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf}{OAI:Koebes-Circle-Domain-Conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalization proves the removability-to-rigidity direction of the He–Schramm conjecture. If a circle domain has conformally removable boundary, then every conformal equivalence from it to another circle domain agrees on the source with a Möbius transformation. There is no bound on the number of complementary components.

The same Comparator file also states Koebe's circle-domain theorem, which gives a circle-domain representative for every domain in the Riemann sphere.

Koebe's circle-domain conjecture asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, whose complementary components are round disks or points. The formalization proves this for every domain. It also proves rigidity under a separate hypothesis: a conformal equivalence between circle domains is a Möbius transformation when the source boundary is conformally removable.

Comparator links

ResultComparator statement
Removable-boundary rigidity and the circle-domain theoremKoebeCircleDomains.lean
Koebe's circle-domain theorem and removable-boundary rigidityKoebeCircleDomains.lean

Scope note on GitHub →