He-Schramm rigidity conjecture: circle domains with conformally removable boundary are rigid
A circle domain is conformally rigid if every conformal equivalence from onto another circle domain is the restriction of a Mobius transformation. A compact set is conformally removable if every orientation-preserving homeomorphism of the sphere that is conformal off is Mobius. He and Schramm proved rigidity for countably connected circle domains and for boundaries of -finite length, and conjectured that a circle domain is rigid if and only if its boundary is conformally removable. Rajala (2025) disproved the rigid-implies-removable direction. Is every circle domain whose boundary is conformally removable conformally rigid?
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Geometric function theory; conformal rigidity and removability
- Posed by
- Zheng-Xu He and Oded Schramm, in their work on rigidity of circle domains (Invent. Math. 1994)
- Year posed
- 1994
- Years open
- 32y
- 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
- 32 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Claims that every circle domain whose boundary is conformally removable is conformally rigid, with no bound on the number of complementary components and no boundary-extension hypothesis on the map. An intermediate theorem shows that a function continuous across a compact totally disconnected removable set with finite Dirichlet energy off it is globally Sobolev. Together with Rajala's counterexample this settles both directions of the He-Schramm equivalence: removable implies rigid, the converse fails. It does NOT characterize rigid circle domains.
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. It uses the quantitative transfer and selection theorem of the companion Koebe manuscript.
Verification
No independent mathematician has checked this yet. Theorem 1.1 was read against the conjecture as the manuscript states it; it proves exactly the removable-implies-rigid direction, the other direction having been disproved by Rajala. 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. removability_implies_rigidity says that for circle domains U and V with conformally removable frontier of U (compact, and every orientation-preserving sphere homeomorphism conformal off it is Mobius), every conformal equivalence f from U onto V agrees on U with a Mobius map. That is the headline claim. The proof depends on the companion Koebe manuscript, also unreviewed.
Sources
- PaperCompanion: Koebe's Circle-Domain Conjecture (supplies the transfer theorem used here)
- 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: Removable Boundaries and Rigidity of Circle Domains
- Problem recordHe and Schramm (1994), rigidity of circle domains with sigma-finite boundary