Aftermath bot: New page for family 071: Koebe circle-domain conjecture with public kernel replays and reviews

2026-10-25T23:36:46Z

New page for family 071: Koebe circle-domain conjecture with public kernel replays and reviews

New page

A '''circle domain''' is a domain in the Riemann sphere whose complementary components are closed round disks or single points. '''Koebe's circle-domain conjecture''' (the ''Kreisnormierungsproblem'', 1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claim the conjecture for every domain, and claim that a circle domain with conformally removable boundary is conformally rigid, one direction of a conjecture of He and Schramm. The collection states both theorems in its Lean formalization. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introductions of the manuscripts:
** Koebe posed the problem in 1908 and proved the finitely connected case. He and Schramm established the countably connected case and proved rigidity for countably connected circle domains (''Ann. of Math.'' 137, 1993); their later rigidity theorem allows uncountably many complementary components when the boundary has σ-finite linear measure. Schramm introduced transboundary extremal length and proved further uniformization results.
** Esmayli and Rajala proved uniformization for cospread domains, and more generally under a uniform quasitripod condition and a packing bound. Karafyllia and Ntalampekos established the conjecture for spherical Gromov-hyperbolic domains ([https://arxiv.org/abs/2405.13782 arXiv:2405.13782]). Rajala showed that arbitrary interior exhaustions can fail to have circle-domain limits.
** A circle domain is ''conformally rigid'' if every conformal map from it onto another circle domain is a Möbius transformation. He and Schramm conjectured that a circle domain is rigid if and only if its boundary is conformally removable. Rajala constructed a rigid circle domain with non-removable boundary, so rigidity does not imply removability. Younsi, Ntalampekos and Younsi, and Ntalampekos proved rigidity under additional geometric or extremal-distance hypotheses on the boundary.
* In a survey of conformal rigidity submitted on 30 September 2026, before the collection was published, Ntalampekos describes Koebe's conjecture as open and asks whether every circle domain with conformally removable boundary must be conformally rigid, noting that this was open even when the whole boundary is a Cantor set ([https://arxiv.org/abs/2610.00560v1 arXiv:2610.00560], section ''Remaining implication in the rigidity conjecture'').

== The original results ==
* '''Koebe's circle-domain conjecture (23 September 2026).''' Theorem 1.1 of the manuscript states that every nonempty connected open subset of the Riemann sphere is conformally equivalent to a circle domain. No condition is imposed on the complement, whose components may be uncountably many.
** ''Method, as described:'' analytic tests on the domain, real functions or functions with additive period one around a selected complementary component, are chosen before finite uniformization. They have finite Dirichlet energy and square-summable boundary oscillation. A transfer theorem carries finitely many tests to finitely connected completions that keep the original conformal structure on a compact core. A duality for path laws, in the form of Fuglede's modulus and the duality of Ambrosio, Di Marino and Savaré, gives either a small barrier around an end or a law of paths reaching it. A four-path crossing argument shows that only countably many ends lack small barriers, so all other complementary components collapse to points. Period-one tests and a Stokes estimate exclude any protrusion beyond the round disks found at the remaining components.
** Combined with an exhaustion theorem of Ntalampekos and Rajala, the manuscript deduces that every proper domain has an exhaustion by finitely connected domains whose normalized circle-domain uniformizations converge to a circle-domain uniformization of the whole domain. This asserts the existence of a suitable exhaustion, not convergence for arbitrary exhaustions.
** Through Theorem 1.1(a) of Luo and Wu ([https://arxiv.org/abs/1910.08001 arXiv:1910.08001]), a corollary in the final section states that every complete hyperbolic surface of genus zero is isometric, in its intrinsic path metric, to the boundary of the hyperbolic convex hull of a compact set in the sphere at infinity whose components are closed round disks or points.
* '''Removable boundaries and rigidity of circle domains (23 September 2026).''' Theorem 1.1 of the companion manuscript states that every circle domain with conformally removable boundary is conformally rigid, with no restriction on the number of complementary components.
** ''Method, as described:'' an intermediate theorem shows that, for a compact totally disconnected set that is conformally removable, a scalar function continuous across the set with finite Dirichlet energy on its complement is globally Sobolev. The proof uses the quantitative retained-test form of the circle-domain theorem from the companion, a conductivity deformation built from the Beltrami equation, and barriers whose energy forces every omitted component to be a point. For a conformal map between circle domains, masks around disk-containing pairs, slice estimates on lines and a flux inequality compared with area bounds force the map to be Möbius.
* '''Source.''' Commit <code>1581d4c</code> of the openai/math repository, folders [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026 Koebe's circle-domain conjecture] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026 Removable boundaries and rigidity of circle domains].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/071.md lean/docs/071.md] states that the formalization proves the removability-to-rigidity direction of the He–Schramm conjecture with no bound on the number of complementary components, and that the same Comparator file states Koebe's circle-domain theorem for every domain in the Riemann sphere. The Comparator challenge is [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/KoebeCircleDomains.lean KoebeCircleDomains.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 26 October 2026)
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/4e9beba0ca689365e70fcd01303775f21a687540/corpus/openai-math/kernel-runs/38040214623/KoebeCircleDomains.json cert-machine], openai/math lane K, run 38040214623 (<code>KoebeCircleDomains</code>) || Verification (kernel replay) || Records that Lean's default kernel and the nanoda kernel both accept the solution, after a run of 4,115 seconds. || Repository.
|-
| 2026-10-10 || [https://github.com/nealmcb/openai-math-lean-tooling/blob/c9570a82f79b78a1a969a6316ac0fdd69aabef55/results/cmp-all/all.jsonl nealmcb/openai-math-lean-tooling] (GitHub; Comparator results at commit <code>c9570a8</code>) || Verification (Comparator replay) || Its Comparator run over the collection's 416 challenge configurations records <code>KoebeCircleDomains</code> as accepted, in a run started on 10 October 2026, without the nanoda kernel. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all 416 Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (failures, time-outs and memory overruns) does not list <code>KoebeCircleDomains</code>, so the challenge is among the 401 accepted by both con-leche and Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee reviews [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_030.json rank_030] (circle-domain theorem) and [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_037.json rank_037] (rigidity) in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
| Review (AI-assisted audit)
| Reports no gap found in either manuscript. For the circle-domain theorem, the reviewer states that it read every section in full except the hyperbolic-surface corollary, which it skimmed, and re-derived the main steps by hand, and that none of this was machine-checked. For the rigidity theorem, its one minor note is a coverage caveat, not an identified error: the quantitative input imported from the circle-domain manuscript (its Theorem 7.5) was not re-audited in that review, and the main theorem depends on it; the reviewer found no circular dependence.
| The reviews are published under CC BY 4.0.
|-
| 2026-10-25 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, [https://github.com/mathvet/mathvet/blob/899d421729f1e4c5f08d302773762b141c52b845/reviews/openai-math/fidelity-table.csv tables] at repository commit <code>899d421</code>, 25 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a sandboxed Comparator pass for the challenge <code>KoebeCircleDomains</code>. Its note says that both the existence part of Koebe's conjecture and the removability-to-rigidity implication are stated for arbitrary domains, and that conformality on the Riemann sphere is encoded chartwise by a custom definition, which it checks against holomorphy with nonzero derivative. || Repository.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Koebe's circle-domain conjecture - Revision history

Aftermath bot: New page for family 071: Koebe circle-domain conjecture with public kernel replays and reviews