OpenAI claim summary for Math-348
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
Circle-domain uniformization: The manuscript’s result quantifies over every nonempty connected open set in the sphere and gives a conformal bijection to a circle domain, exactly the definition including arbitrary complement cardinality; no rigidity or boundary regularity is required.
With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Koebe circle-domain uniformization conjecture
OpenAI's claim
Circle-domain uniformization: Every connected open region of the Riemann sphere is claimed to have a conformal representative whose missing components are disks or single points. The assertion allows infinitely many boundary components.Mathematical statement of the claimed result
Mathematical claim 1.
For a nonempty connected open set $G\subset\widehat{\mathbb C}$, there are a domain $\Omega\subset\widehat{\mathbb C}$ and a conformal bijection $f:G\to\Omega$ such that every connected component of $\widehat{\mathbb C}\setminus\Omega$ is either a closed round disk or a singleton. The number of complementary components is unrestricted.Outline of the argument
Circle-domain uniformization: The argument replaces complementary components by labels on a quotient sphere, then transfers finitely many boundary tests to conformal completions while keeping their periods and controlling their energy. A barrier-versus-path-law alternative supplies additional tests, and a fusion construction handles all boundary labels together. Exhaustion by finite circle models yields a limiting map; the accumulated tests exclude a nonround limiting hole.Formal verification
Family 071 describes Lean coverage for the universal circle-domain representative and the Möbius rigidity implication under removable source boundary.Circle-domain uniformization: The manuscript links KoebeCircleDomains.lean.
The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, Koebe's Circle-Domain Conjecture, 2026-09-23; citation key
OAI:Koebes-Circle-Domain-Conjecture-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 071: Lean scope.
- Comparator KoebeCircleDomains.json.
- Comparator KoebeCircleDomains.lean.
- OpenAI catalogue entry.