Koebe's circle-domain conjecture (Kreisnormierungsproblem)
A circle domain is a domain in the Riemann sphere each of whose complementary components is a closed round disk or a single point. Koebe proved that every finitely connected domain is conformally equivalent to a circle domain, and He and Schramm (1993) extended this to countably connected domains. Koebe's Kreisnormierungsproblem, posed in 1908, asks for the general case, with no restriction on the number or shape of the complementary components, which may be uncountably many. Is every domain conformally equivalent to a circle domain?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Geometric function theory; conformal uniformization
- Posed by
- Paul Koebe, Uber die Uniformisierung beliebiger analytischer Kurven, Dritte Mitteilung (Nachr. Ges. Wiss. Gottingen, 1908)
- Year posed
- 1908
- Years open
- 118y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 60 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Claims that every domain in is conformally equivalent to a circle domain, with no countability or geometric condition on the complementary components. The method marks countably many components, collapses unmarked ones to points with small energy barriers, and shows marked ones become exactly round disks, using transboundary extremal length and a modulus-probability duality. Combined with Ntalampekos-Rajala it also gives a convergent exhaustion by finitely connected domains. It does NOT give uniqueness of the circle-domain model; the rigidity question is the companion's subject and is answered there only under conformal removability of the boundary.
What the AI did
The release README says the manuscripts were produced by an unreleased internal OpenAI model, the vast majority by one fixed procedure using on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier results produced by the models. Its named exceptions to that procedure (the Hodge conjecture for CM abelian varieties and the zeta zero-free region work) do not concern this family. The manuscript is credited to OpenAI with no human author named.
Verification
No independent mathematician has checked this yet. Theorem 1.1 was read against Koebe's problem as the manuscript and its references state it: every nonempty connected open subset of the sphere is conformally equivalent to a circle domain, with no condition on the complement. The Lean challenge ComparatorChallenges/KoebeCircleDomains.json (solution module OAI.Analysis.CircleDomains.Main, present at the pinned commit) is not in the formalization catalogue formalization.yaml; it was found through lean/docs/071.md. It compares two theorems, OAI.Problem047.koebe_circle_domain and OAI.Problem047.removability_implies_rigidity, with permitted axioms propext, Quot.sound and Classical.choice. The statement was read here; not rebuilt here. koebe_circle_domain says every open connected U in the one-point compactification of C admits a set V and a map f with V a circle domain (open, connected, each complementary component a point or a Mobius image of the closed unit disk) and f a conformal equivalence of U onto V (nonzero complex derivative in charts at every point, with a conformal inverse). That is the headline claim. Uniqueness up to Mobius maps is not claimed here and is false in general.
Sources
- PaperCompanion: Removable Boundaries and Rigidity of Circle Domains
- Lean proofLean: solution module (koebe_circle_domain, removability_implies_rigidity)Lean comparator statement: circle-domain theorem and removable-boundary rigidityLean: release scope note for this family
- CodeOpenAI math release: Koebe's Circle-Domain Conjecture
- Problem recordKoebe (1908), digitized article record