Koebe’s circle-domain conjecture

The explanation

Take the whole plane and cut out one round hole. Treat each point as a complex number, so the point (2, 1) is 2+i. Let the hole be the disk of radius 1 around the point 2. Now apply the flip that sends each point z to 1/z. The hole's edge points 1 and 3 land on 1 and 1/3. The edge point 2+i lands on 0.4−0.2i. All three now sit exactly 1/3 away from the point 2/3. In fact the whole edge circle lands on the circle of radius 1/3 around 2/3. The round hole stays round. It only moves and shrinks.

The flip is a conformal map. It bends the picture but keeps the angle between any two crossing curves. Now start with a hole of another shape, such as a square. Can a conformal map always make it round? Koebe asked a much bigger version of this in 1908. A domain is a connected open region: one piece, with its edge left out. The Riemann sphere is the plane plus one extra point at infinity. A circle domain is a domain on that sphere whose missing pieces are all closed round disks or single points. Koebe asked whether every domain is conformally equivalent to a circle domain. That means one conformal map carries it exactly onto a circle domain.

For finitely many holes, the answer was known to be yes. Koebe proved that case; the paper cites his 1920 treatment. In 1993, Zheng-Xu He and Oded Schramm proved it for countably many holes. Countably many means the holes can be listed one after another. Schramm gave another proof in 1995 with a tool called transboundary extremal length. Later work reached some regions with even more holes. Esmayli and Rajala, and separately Karafyllia and Ntalampekos, did this under geometric conditions on the holes.

The hard case is a region with uncountably many holes. These holes can have any shape. Nothing keeps them apart from each other. The natural plan approximates the region by regions with finitely many holes. Koebe's theorem makes those holes round. Then one passes to a limit. But in the limit, a hole can hold more than the round disk being followedSource 1. It can carry an extra bulge. Other holes are never followed at all. Kai Rajala showed that a careless choice of approximations can fail to reach a circle domain.

The paper Koebe's Circle-Domain Conjecture proves the full answer, with no condition on the holesSource 2. Every domain on the sphere is conformally equivalent to a circle domainSource 3. Its method picks countably many holes to followSource 4. It argues that every other hole shrinks to a single point. It also argues that every followed hole ends up exactly round, with no bulgeSource 4. So a square hole, a jagged hole and uncountably many specks can all be handled at once.

The first example also shows that the round model is not unique. A Möbius map is a formula (az+b)/(cz+d) with ad−bc not zero. The flip 1/z is one of them. Möbius maps turn one circle domain into another. A circle domain is rigid if these are its only conformal maps onto circle domains. He and Schramm proved rigidity for countably many holes in 1993. In 1994 they allowed uncountably many holes, if the boundary has σ-finite length. That means it splits into countably many pieces of finite length. They conjectured that rigidity holds exactly when the boundary is conformally removable.

Conformally removable describes a closed set E on the sphere. Take any one-to-one, continuous map of the sphere onto itself that keeps orientation. Suppose it is conformal everywhere outside E. The set E is removable if every such map must be Möbius. In 2025, Rajala built a rigid circle domain with a non-removable boundary. So one direction of the conjecture is false. Younsi, then Ntalampekos and Younsi, then Ntalampekos, proved rigidity under extra conditions. The companion paper on removable boundaries proves the other direction in full: a removable boundary makes a circle domain rigidSource 5. The number of holes is unlimitedSource 6. Its proof uses a quantitative part of the Koebe paper's constructionSource 7.

The two results answer different questions, and the gap matters. The Koebe paper says a round model exists for every domain. It does not say that model is unique up to Möbius maps. The removable-boundaries paper gives that uniqueness when the round model has a removable boundary. It says nothing about circle domains with non-removable boundaries.

How sure is this? The release's Lean scope note says a formalization proves both main theorems. It covers existence of a circle domain for every domain. It also covers rigidity when the boundary is conformally removable. One formal statement file states both. Neither paper appears in the release's list of formalized papers, so the scope note is the only record. No specialist review has been published.

What it doesn't show. This does not settle rigidity for circle domains whose boundary is not conformally removable.