Browse › Real and complex analysis › 071 Koebe’s circle-domain conjecture
Koebe's Circle-Domain Conjecture
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 every domain in the Riemann sphere is conformally equivalent to a circle domain, resolving Koebe's circle-domain conjecture positively.
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 covers Koebe's circle-domain theorem for every domain together with removable-boundary rigidity, both stated in one Comparator file. [family-level]
- OpenAI math release, KoebeCircleDomains.lean (Comparator challenge) (openai/math, commit adc7f12). The Comparator statement file has two theorems:
koebe_circle_domain(every domain in the sphere is conformally equivalent to a circle domain) andremovability_implies_rigidity. [family-level]
Related prior literature mentioned by others
- Dimitrios Ntalampekos, Uniformization problems in the plane: A survey (arXiv:2603.15098, 2026-03-16). The AI Proved What? episode points to this survey for the pre-release history of circle-domain uniformization and its associated uniqueness problem. [family-level]
Possibly relevant literature (found by the agent, not checked)
- C. Karafyllia, D. Ntalampekos, Koebe uniformization, John domains, and transboundary modulus (arXiv:2609.31216, 25 Sep 2026). Posted shortly before the release, it proves Koebe's conjecture for John domains and gives a necessary and sufficient condition via Schramm's transboundary modulus, related to the paper's transboundary-type tests; the bibliography cites the same authors' Gromov-hyperbolic paper but not this one.
- Y. Zhong, Koebe uniformization of nondegenerate domains with bounded gap-ratio (arXiv:2408.03484, 2024-08-07). Uses transboundary extremal length to uniformize nondegenerate uncountably connected domains with bounded gap-ratio, a special case of Theorem 1.1; not in the paper's bibliography.
- X. Wang, Y. Zhong, Koebe uniformization for infinitely connected attracting Fatou domains (arXiv:2406.13524, 2024). Proves circle-domain uniformization for infinitely connected attracting Fatou domains of geometrically finite rational maps, a special case of Theorem 1.1; not in the paper's bibliography.
Digests and expositions
- Latent Seminar, Circle-domain uniformization and removable-boundary rigidity (2026-10-06). This exposition outlines retained-test transfer, barriers, periodic tests, and the rigidity companion's trace estimates, explicitly disclaiming independent verification of the complete proofs. [family-level]
- AI Proved What?, Every hole made round? Koebe's circle-domain conjecture (Episode 071, October 2026). This AI-assisted video and transcript explain both manuscripts, their dependence on retained tests, and the distinction between circle-domain existence and rigidity under removability. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 071
Independent sites; their content is not reviewed here.
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}
}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:
- Removable Boundaries and Rigidity of Circle Domains · September 23, 2026