Negative Kähler curvature without bounded holomorphic coordinates

Proves a complete Kähler threefold with pinched negative curvature can lack bounded holomorphic coordinates.

2 papers September 25, 2026 Explained by AI

In one complex dimension, a complete, simply connected surface with curvature below a negative constant is the disc. In higher dimensions, experts asked if two-sided negative curvature forces bounded holomorphic coordinates, as on a bounded domain. The main paper builds a three-dimensional example where this fails, and Lean, a computer proof checker, has a formal statement of it. A companion paper claims a stronger failure when only an upper curvature bound is kept: no nonconstant bounded holomorphic function at all.

First step

1967

Hung-Hsi Wu, question (1) in his work on normal families

Significance

Major

It answers a uniformization question of Wu and of Wu and Yau with a Lean-checked construction, and the companion claims Yau's one-sided problem.

Trust

Formal proof listed

Field

Differential geometry

2 papers

The explanation

Take the unit disc, the complex numbers z with |z| < 1. Give it the Poincaré metric, which has constant curvature −1. The distance from the centre to the point r is 2 artanh r, which equals log((1 + r)/(1 − r)). At r = 0.9 this is log 19, about 2.944. At r = 0.99 it is log 199, about 5.293. As r nears 1 the distance grows without limit, so the metric is complete: the edge is infinitely far away. Yet the coordinate z itself stays smaller than 1. So the disc has a bounded holomorphic coordinate, a bounded function given by a complex power series.

In complex dimension one, a complete simply connected surface with curvature below a negative constant is the discSource 1. In higher dimensions, Wu asked a similar question. Wu and Yau stated a two-sided versionSource 2. Suppose a complete simply connected Kähler manifold has every curvature between two negative constants. Must it be a bounded domain, so that it has bounded holomorphic coordinates? A Kähler manifold is a complex space with a metric that fits its complex structure. Mostow and Siu found examples not covered by the ball, but those did not rule out some other bounded domainSource 3.

The first paper proves the answer is no. It builds a contractible domain in ℂ³ with a complete Kähler metric whose curvatures lie between −B and −A, both negative. No bounded holomorphic map to ℂ³ has a nowhere-zero Jacobian, so the domain is not a bounded domainSource 4. The space is a family of discs over the unit ball in ℂ². The disc above z has radius e^(−φ(z)/2) for a chosen function φSource 5. The obstacle is to pick φ smooth enough for curvature control, yet rough enough to block every bounded holomorphic coordinate. The example still has two nonconstant bounded holomorphic functions, its base coordinatesSource 6.

The second paper drops the lower curvature bound. In some large fixed complex dimension, it claims a domain with curvature at most −1 and only constant bounded holomorphic functionsSource 7. This answers the one-sided question, which Wu and Yau trace to Yau's Problem 38 from 1982Source 8. Its curvature is unbounded belowSource 9. The two constructions and their proofs are independentSource 10.

How sure is this? Lean, a computer proof checker, has a formal statement of the first paper's main result. So that paper proves its construction, as far as the Lean statement matches the paper. The companion's one-sided result is not in the Lean scope and remains a claim. No specialist review of either paper is published.

What it doesn't show. This does not settle whether two-sided pinching forces at least one nonconstant bounded holomorphic function; the main example has two. The companion's curvature is unbounded below, and it has no Lean check.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major for the first result, which has a Lean statement and answers a stated uniformization question. The one-sided companion is a claim without a Lean check. Neither paper has a published specialist review.

Words used

Holomorphic: Given near each point by a convergent power series in complex variables.
Kähler manifold: A complex space with a metric that fits its complex structure.
Complete metric: A metric in which no path of finite length runs off the edge of the space.
Bounded domain: An open connected region inside a finite ball in complex space.
Jacobian: The determinant that tests whether a map is locally one-to-one at a point.
Negatively pinched: Having every sectional curvature between two fixed negative constants.
Contractible: Able to be shrunk continuously to a single point.

The original papers (2)

A negatively pinched Kähler threefold without bounded holomorphic coordinates (PDF, opens in a new tab)
September 25, 2026 Formal proof listed
One-sided negative sectional curvature and the holomorphic Liouville property (PDF, opens in a new tab)
September 25, 2026

Lean notes

All quoted lines (10)

In complex dimension one, a complete simply connected surface whose curvature is bounded above by a negative constant is biholomorphic to the disk.
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
Wu and Yau state the two-sided real-sectional version with a bounded pseudoconvex domain as conclusion: if a simply connected complete K\"ahler manifold has every real sectional curvature between two negative constants, must it be biholomorphic to a bounded domain in its complex dimension?
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
These non-ball results, however, do not exclude a biholomorphism to some other bounded domain; that is the stronger obstruction sought here.
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
No bounded holomorphic map $F:M\to\C^3$ has a nowhere-vanishing Jacobian determinant.
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
Thus the disc above $z$ has radius $e^{-\phi(z)/2}$ .
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
The example has two bounded nonconstant holomorphic functions, supplied by its base coordinates.
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text
For some finite integer $m\ge2$ there is a domain $\mathcal T\subset\mathbb C^m$ , diffeomorphic to $\mathbb R^{2m}$ , with a complete K\"ahler metric $g$ such that $\operatorname{Sec}_g\le-1, \qquad H^\infty(\mathcal T)=\mathbb C.$
One-sided negative sectional curvature and the holomorphic Liouville property Back to text
We use the public formulation recorded by Wu and Yau; their survey traces it to Yau's 1982 Problem 38.
One-sided negative sectional curvature and the holomorphic Liouville property Back to text
The sectional curvatures of $g$ are unbounded below.
One-sided negative sectional curvature and the holomorphic Liouville property Back to text
The two constructions and their proofs are independent.
A negatively pinched Kähler threefold without bounded holomorphic coordinates Back to text

Other sources

openai/math, Lean scope note for family 359 Nevertheless, it has no system of bounded holomorphic coordinates and is not biholomorphic to a bounded domain.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

358A three-manifold without conjugate points or nonpositive curvatureDifferential geometry
360Weak MTW curvature gives convexity and regular optimal transportDifferential geometry
361Failure of integer-degree harmonic dimension comparisonDifferential geometry
356Gigli’s characterization of Alexandrov curvatureDifferential geometry
352A finite-time singularity of Calabi flowDifferential geometry

Browse Differential geometry Curvature and geometric flows Open since the 1960s Lean-checked results