The Wu–Yau bounded-domain conjecture
From OpenAI Aftermath
The Wu–Yau bounded-domain conjecture asks whether a simply connected complete Kähler manifold whose real sectional curvatures all lie between two negative constants must be biholomorphic to a bounded domain in its complex dimension. In complex dimension one the answer is yes, by uniformization. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 25 September 2026, claim a counterexample in complex dimension three and, in a large fixed dimension, a negative answer to Yau's related question on bounded holomorphic functions under a one-sided curvature bound, with a Lean formalization of the first claim. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- H. Wu asked in 1967 whether a complete simply connected Kähler manifold with nonpositive real sectional curvature and holomorphic sectional curvature bounded above by a negative constant is biholomorphic to a bounded domain. Wu and Yau state the version with two-sided negative bounds on every real sectional curvature as Conjecture 4.3 of their 2019 survey.
- Mostow and Siu constructed compact negatively curved Kähler surfaces not covered by the ball, and Deraux obtained three-dimensional examples; these do not exclude a biholomorphism to some other bounded domain. Under two-sided pinching, Greene and Wu, and later Wu and Yau, compared the Bergman, Kobayashi–Royden and complete Kähler–Einstein metrics with the original metric; these comparisons do not supply bounded holomorphic coordinates.
- The weaker question, whether an upper bound by a negative constant alone forces a nonconstant bounded holomorphic function, is recorded by Wu and Yau and traced to Yau's 1982 Problem 38. Seshadri's complete Kähler metric on ℂn with strictly negative sectional curvature shows that a uniform negative upper bound is essential to that question.
The original results
- Claim (pinched threefold). The main theorem of A negatively pinched Kähler threefold without bounded holomorphic coordinates states that there are a contractible domain M in ℂ3 and a smooth complete Kähler metric on M whose real sectional curvatures lie between −B and −A for constants 0 < A ≤ B, such that no bounded holomorphic map from M to ℂ3 has a nowhere-vanishing Jacobian; in particular M is not biholomorphic to a bounded domain. The manuscript notes that M is Stein and has two nonconstant bounded holomorphic functions, its base coordinates.
- Claim (one-sided companion). Theorem 1.1 of One-sided negative sectional curvature and the holomorphic Liouville property states that for some finite dimension m ≥ 2 there is a domain in ℂm, diffeomorphic to Euclidean space, with a complete Kähler metric of sectional curvature at most −1 and only constant bounded holomorphic functions. Its sectional curvatures are unbounded below, and the manuscript states that the bounded-function question under a two-sided bound remains separate.
- Method, as described: the threefold is a family of discs over the unit ball in ℂ2, the disc over z having radius e−φ(z)/2, with a Kähler potential of Calabi type. Cauchy estimates turn a bounded map with nowhere-vanishing Jacobian into a holomorphic function whose real part stays below φ plus a logarithmic boundary allowance. The weight φ is built from homogeneous peaks with radial corrections, so that positive probabilities on spheres preserve holomorphic averages while the averages of the tested function tend to −∞. A cancellation on degenerate planes gives the curvature pinching for one large base parameter. The companion builds a tube over a complete nonpositively curved Kähler potential, which gives curvature at most −1, and places large holomorphic testing discs over grids of polynomial zeros; Cauchy estimates on these discs show that every bounded holomorphic function is independent of the tube variable, so it descends to a bounded entire function on the base and is constant.
- Sources (openai/math repository, commit
7ef5c0c): A negatively pinched Kähler threefold without bounded holomorphic coordinates (25 September 2026); One-sided negative sectional curvature and the holomorphic Liouville property (25 September 2026). - Formalization, as described by the repository. The scope note lean/docs/359.md states that the formalized result constructs a nonempty contractible complex threefold with a complete Kähler metric whose real sectional curvatures lie between two fixed negative constants, with no system of bounded holomorphic coordinates and no biholomorphism to a bounded domain, the metric being obtained from an explicitly controlled potential. It states that the companion with one-sided curvature control is separate. The Comparator statement is
PinchedKahler.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Negative Kähler curvature: bounded coordinates and the holomorphic Liouville property, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains Kähler potentials and bounded holomorphic functions, the two constructions and their curvature hypotheses, the disc family and the Jacobian obstruction, representing probabilities and negative logarithmic averages, completeness and the pinching estimate, and the companion's tube and large testing discs, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": the Lean statement gives the contractible domain in ℂ3 with a complete pinched Kähler metric, no bounded holomorphic map with nowhere-vanishing Jacobian and no biholomorphism onto a bounded domain, while the companion's higher-dimensional example is not stated. It notes that the Kähler geometry, including curvature and geodesic completeness, is hand-coded, and that the formal statement excludes every bounded holomorphic map with nowhere-vanishing Jacobian, which is stronger than excluding injective coordinates. It records a Comparator pass on cloud machines for PinchedKahler on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the PinchedKahler solution, in 929 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list PinchedKahler, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_205 (one-sided companion) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. It adds one minor note, which it states is a limit on verification and not a demonstrated gap: several steps in Sections 5, 7 and 8 pack many exponent comparisons into one sentence; the reviewer spot-checked the leading exponents but did not re-derive every budget inequality, and skimmed Sections 5 and 7 through their use in Section 8. The reviewer reports a numerical check of the six curvature blocks against a direct curvature computation on an explicit example and a symbolic check of the radial curvature components. | Part of an audit that its README describes as complete for the collection's manuscripts without a Lean formalization; the pinched-threefold manuscript is not among them. The reviews are published under CC BY 4.0. |
| 2026-10-19 | AI Proved What?, episode 359 Pinched negative, no bounded domain?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the two claims and their history. The episode states that the first example has nonconstant bounded functions and the second has curvature unbounded below, so that neither settles whether pinched curvature gives one nonconstant bounded function, that neither treats complex dimension two, and that the second paper's dimension is not given explicitly. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, 36 + 58 pages, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the first paper's main theorem and two key propositions, not the second paper. The page states that it found no specialist comment and no reported error. |
Notes
- The background summarizes the manuscripts' own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
