AI Proved What?

Episode 071, October 2026

Every hole made round?

Koebe’s circle-domain conjecture

Covers result 071 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

Play Episode 071: Every hole made round? A rounded frame with irregular orange holes and an arrow down to the same frame with round teal holes, above the formula G is conformally equivalent to a circle domain.

6:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Round holes
  2. 1:25The claim
  3. 2:27Collapse or protrude
  4. 4:30Rigidity
  5. 5:26Where it stands

The claims, in plain words

The Riemann mapping theorem says that every simply connected domain in the plane, other than the plane itself, can be mapped conformally, preserving angles, onto the round disk. Domains with holes have more shape: a ring can be mapped onto a round annulus, but the ratio of its radii cannot be changed. In 1908 Koebe asked whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary pieces are all round disks or single points.

Koebe proved this for finitely many holes. In 1993 He and Schramm proved it for countably many, and Schramm later introduced transboundary extremal length. Other work handled domains with geometric conditions (Esmayli and Rajala; Karafyllia and Ntalampekos). The hard case has uncountably many complementary pieces, of any shape, with no regularity assumed at all.

A second question is uniqueness. For countably many holes the round model is unique up to Möbius transformations. If the complement is a Cantor set of positive area, a map can be conformal away from the set without being Möbius, and uniqueness fails. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable; Rajala showed that rigidity does not imply removability.

Result 071 is two OpenAI preprints, both dated September 23, 2026. The first (64 pages) claims Koebe’s conjecture with no restriction on the domain: every domain in the Riemann sphere is conformally equivalent to a circle domain. The second (25 pages) claims the other direction of He and Schramm’s conjecture: a circle domain whose boundary is conformally removable is rigid, so every conformal map onto another circle domain is a Möbius transformation. The Koebe paper also derives convergent exhaustions by finitely connected pieces and a realization of every complete genus-zero hyperbolic surface as the boundary of a hyperbolic convex hull.

What they don’t claim

An exact description of which circle domains are rigid. Rajala’s examples show that some rigid circle domains have non-removable boundaries, so removability is sufficient but not necessary.

Where it stands

Posted as preprints
OpenAI, both dated September 23, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
Both theorems, by OpenAI (scope note); we have not run the check

Last checked October 19, 2026. Neither preprint has been revised. OpenAI’s scope note says its Lean formalization proves both theorems; the formal statements are proved in a folder of about 2,600 files and 211,000 lines with no unfinished proofs, which we have not built. The rigidity paper uses a quantitative transfer theorem from the Koebe paper, and neither cites papers from other results in the release. Inputs include Koebe’s finite theorem, Schramm’s transboundary approach, the modulus–probability duality of Ambrosio, Di Marino and Savaré, Moore’s decomposition theorem and the Beltrami equation. We found no public assessment by specialists; a recent survey describes the state of the problem before the release.

How the proofs go

  1. Finite pictures. Collapse each complementary piece to a point; the result is again a sphere, and the collapsed points form a compact, totally disconnected set of labels. Finitely connected approximations that keep the domain’s own conformal structure on a large core have circle-domain models by Koebe’s finite theorem, and their limit is a candidate. It can fail in two ways: a piece may not shrink to a point, or a piece that should be a disk may carry a protrusion.
  2. Barriers. A function equal to one near a piece and zero near an anchor is a barrier; its cost is its Dirichlet energy plus a charge for its jumps across other pieces. With nothing else in the way, fencing off a disk of radius r inside the unit circle costs at least 2π/log(1/r): tending to zero for a point, bounded below for a disk. Cheap barriers force pieces to collapse.
  3. Countably many marked pieces. Each piece has a cheap barrier or a probability law on paths reaching it; a four-path crossing argument shows that only countably many lack cheap barriers. For those, tests with period one around the piece, built from averaged step functions that jump across random arcs, bound a boundary integral that a protrusion would push higher.
  4. Transfer. The tests are transferred to finite approximations with arbitrarily little extra energy, keeping the original structure on growing cores, so the limit map is conformal and its image is a circle domain.
  5. Rigidity. On the complement of a compact, totally disconnected, removable set, a function continuous across the set with finite Dirichlet energy is Sobolev on the whole sphere. For a conformal map between circle domains, the pairs involving disks are masked, the scalar theorem is applied to the common point pieces, and slice estimates give a flux inequality; comparison with the area bounds forces equality and a Möbius map.

The numbers in the video

  • A short Python script derives the least barrier energy 2π/log(R/r) across an annulus (2.73, 1.36, 0.68, 0.34 and 0.17 around a point for r = 10−1 down to 10−16; 9.06 around a disk of radius 1/2), counts 3n − 6 real moduli of n-connected domains, checks that a Möbius map sends a circle to a circle, and computes that a fat Cantor set of length 1/2 has a square of area 1/4.

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Round holes

The Riemann mapping theorem says that every simply connected domain in the plane, other than the plane itself, can be mapped conformally, preserving angles, onto the round disk. Domains with holes have more shape. A ring can be mapped onto a round annulus, but the ratio of its radii cannot be changed. In 1908, Koebe asked whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary pieces are all round disks or single points. Koebe proved this for finitely many holes. In 1993, He and Schramm proved it for countably many, and Schramm later introduced transboundary extremal length. Other work handled domains with geometric conditions, such as those of Esmayli and Rajala, and of Karafyllia and Ntalampekos. The hard case has uncountably many complementary pieces, of any shape, with no regularity assumed at all. A second question is uniqueness: is the round model unique up to Möbius transformations? For countably many holes, yes. But if the complement is a Cantor set of positive area, a map can be conformal away from the set without being a Möbius transformation, and uniqueness fails. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rajala showed that rigidity does not imply removability.

1:25The claim

Result 071 is two OpenAI preprints, both dated September 23. The first, 64 pages, claims Koebe’s conjecture with no restriction on the domain: every domain in the Riemann sphere is conformally equivalent to a circle domain. The second, 25 pages, claims the other direction of He and Schramm’s conjecture: a circle domain whose boundary is conformally removable is rigid, so every conformal map onto another circle domain is a Möbius transformation. OpenAI also published a Lean formalization that it says proves both theorems, about 2,600 files in its own folder with no unfinished proofs; we have not run it. The Koebe paper also derives two consequences: suitable exhaustions by finitely connected pieces whose circle-domain maps converge, and a realization of every complete hyperbolic surface of genus zero as the boundary of a hyperbolic convex hull.

2:27Collapse or protrude

The proof starts from finite pictures. Collapse each complementary piece to a point. The result is again a sphere, and the collapsed points form a compact, totally disconnected set of labels. Finitely connected approximations, which keep the domain’s own conformal structure on a large core, have circle-domain models by Koebe’s finite theorem, and a limit of these maps gives a candidate. Two things can go wrong. A limiting piece may fail to shrink to a point, or a piece that should be a disk may carry an extra protrusion. The tool is energy. A function equal to one near a piece and zero near a fixed anchor acts as a barrier, and its cost is its Dirichlet energy plus a charge for how much it jumps across the other pieces. With nothing else in the way, fencing off a disk of radius r inside the unit circle costs at least 2π/log(1/r). For a point, r can be as small as we like, so the cost tends to zero; for a genuine disk it stays bounded below. So cheap barriers force pieces to collapse to points. The paper proves an alternative: each piece either has such a barrier, or there is a probability law on paths that reach it with controlled length. A four-path crossing argument shows that only countably many pieces can lack cheap barriers. Those are marked. For each, either a cheap barrier rules out a protrusion, or tests with period one around the piece, built by averaging step functions that jump by one across random arcs running into it, bound a boundary integral, and a protrusion would push that integral strictly higher. So in the limit every marked piece is exactly its disk. To make this work, the tests are transferred to the finite approximations with arbitrarily little extra energy. The original conformal structure is kept on a growing core, while the structure outside it may change. The cores exhaust the domain, so the limit map is conformal, and its image is a circle domain.

4:30Rigidity

For rigidity, removability must be used before the map is known to extend to the sphere. The second paper first proves a scalar statement: on the complement of a compact, totally disconnected, removable set, a function that is continuous across the set and has finite Dirichlet energy is a Sobolev function on the whole sphere. To get there, it nearly maximizes a Laurent coefficient at infinity and deforms through the Beltrami equation, producing coordinate barriers of small energy. Then comes the map itself. Under a conformal map between circle domains, a point piece may correspond to a disk. The paper masks the countably many pairs involving disks, applies the scalar theorem to the common point pieces, and integrates slice estimates into a flux inequality. Comparing it with the area bounds forces equality, and that forces the map to be a Möbius transformation.

5:26Where it stands

Neither preprint is peer reviewed, and neither has been revised. OpenAI reports a Lean formalization of both main theorems; we have not run the check. The rigidity paper uses a quantitative transfer theorem from the Koebe paper, and neither cites papers from other results in the release. Inputs include Koebe’s finite theorem, Schramm’s transboundary approach, the modulus and probability duality of Ambrosio, Di Marino and Savaré, Moore’s decomposition theorem, and the Beltrami equation. We found no public assessment. If it holds, Koebe’s problem from 1908 is solved: every domain in the sphere has a round model, and that model is unique up to Möbius maps whenever its boundary is conformally removable. An exact description of which circle domains are rigid is not claimed.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.