A negatively pinched Kähler threefold without bounded holomorphic coordinates

Lean formalization in OpenAI math repository (Result 359)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A negatively pinched Kähler threefold without bounded holomorphic coordinates'. We construct a contractible domain in complex dimension three with a complete Kähler metric whose real sectional curvatures lie between two finite negative constants. It admits no bounded holomorphic map to ℂ3 with nowhere-vanishing Jacobian and is therefore not biholomorphic to a bounded domain. This gives a negative answer to the negatively pinched Kähler uniformization question.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 359). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository