we-solve (beta)

Math-258-A2 · revision r1 · on Math-258

OpenAI claim summary for Math-258

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Manuscript 1 (family 046, 2026-10-05): The projective fourfold’s universal cover is non-Stein and has no positive-dimensional compact analytic subvariety; holomorphic convexity would then have a zero-dimensional Remmert reduction fiber and force Steinness, so this is a counterexample.

Manuscript 2 (family 046, 2026-09-23): The main theorem constructs a smooth projective complex surface with a noncompact holomorphic hull in its universal cover, directly negating the catalogue holomorphic-convexity requirement.

Manuscript 3 (family 058, 2026-09-24): The Remmert-reduction corollary proves holomorphic convexity under a semialgebraic projective-open presentation of the universal cover; the catalogue requires no semialgebraicity.

Manuscript 4 (family 058, 2026-09-24): For a projective manifold whose universal cover meets the bounded semialgebraic-domain and compact-quotient hypotheses, symmetry makes that cover Stein and hence holomorphically convex; general projective universal covers need not satisfy these hypotheses.

Manuscript 5 (family 067, 2026-09-25): The nef-tangent uniformization corollary yields a compact homogeneous factor times affine space and hence holomorphic convexity in the stated dimension-at-most-six or bounded Albanese-fiber class; the catalogue allows arbitrary projective varieties.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Holomorphic Convexity of Universal Covers
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Manuscript 3.
  7. Manuscript 4.
  8. Manuscript 5.
  9. Outline of the argument
  10. Formal verification
  11. Status caveat
  12. Sources

Holomorphic Convexity of Universal Covers

OpenAI's claim

Manuscript 1 (family 046, 2026-10-05): A smooth complex fourfold is claimed to be projective, to have large fundamental group, and to have a non-Stein universal cover lacking positive-dimensional compact analytic subvarieties; Manuscript 2 (family 046, 2026-09-23): OpenAI claims a smooth projective complex surface whose universal cover fails holomorphic convexity, giving a two-dimensional counterexample. Manuscript 3 (family 058, 2026-09-24): A normal projective universal cover is claimed to have a semialgebraic projective model exactly when it decomposes into a symmetric bounded-domain factor, a complex affine-space factor, and a simply connected normal projective factor; Manuscript 4 (family 058, 2026-09-24): With cocompact biholomorphisms, a connected semialgebraic bounded open set in a complex affine variety is claimed to be smooth and biholomorphically equivalent to a symmetric domain that is bounded. Manuscript 5 (family 067, 2026-09-25): Among smooth complex Fano varieties in dimension six, those with nef tangent are claimed to be rational homogeneous, with a universal-cover consequence when dimension minus maximal étale irregularity is at most six.

Mathematical statement of the claimed result

Manuscript 1.
OpenAI claims a smooth connected projective complex fourfold $X$ containing a simple abelian surface $A$ such that $X$ has large fundamental group and \[ \operatorname{im}(\pi_1(A)\to\pi_1(X))\simeq\mathbb Z, \qquad\widetilde X\text{ is not Stein}. \] Large means that for every positive-dimensional irreducible closed subvariety $Z$, the image of $\pi_1(Z^\nu)$ in $\pi_1X$ is infinite. The simply connected universal cover is claimed to have no positive-dimensional compact analytic subvariety. This disproves the Stein assertion with the large-group hypothesis.
Manuscript 2.
OpenAI claims a smooth connected projective complex surface $X$ with a connected nodal curve $Z_0$ each of whose irreducible components is rational and smooth, and for which the image of $\pi_1(Z_0)\to\pi_1(X)$ is infinite. In its simply connected cover, a connected lift of $Z_0$ is a closed noncompact union of compact rational curves, locally finite as a family. It claims for any point $x$ on that lift that \[ \widehat{\{x\}}_{\widetilde X}=\{y:|g(y)|\le|g(x)|\text{ for every }g\in\mathcal O(\widetilde X)\} \quad\text{is noncompact}. \] Consequently this universal cover is not holomorphically convex.
Manuscript 3.
For any connected normal projective complex variety $X$, OpenAI claims equivalence between its ordinary universal cover being biholomorphic to an open semialgebraic subset in some projective variety and a decomposition \[ \widetilde X\simeq D\times\mathbb C^m\times F, \] where $m\ge0$, $D$ is a bounded symmetric domain, while $F$ is projective, normal and simply connected; either may be a point. Semialgebraic means finite Boolean operations on real-polynomial equality or inequality conditions in an algebraic presentation. No algebraicity of deck transformations is assumed. The projection to $D\times\mathbb C^m$ is claimed to be the Remmert reduction, proper with connected compact fibers and unchanged holomorphic function sheaf; thus the cover is holomorphically convex and is Stein exactly when $F$ is a point.
Manuscript 4.
Let $U$ be a nonempty connected bounded semialgebraic open subset of a complex affine variety in a fixed closed embedding into $\mathbb C^N$. Suppose a biholomorphism group $\Gamma$ acts properly discontinuously and $U/\Gamma$ is compact. OpenAI claims \[ U\text{ is smooth and biholomorphic to a bounded symmetric domain}. \] A bounded symmetric domain is one in which each point is isolated in the fixed locus of a holomorphic involution. Initial smoothness, freeness of the action, and algebraicity of the biholomorphisms are not assumed.
Manuscript 5.
OpenAI claims rational homogeneity for each smooth connected complex projective Fano manifold of dimension six whose tangent bundle is nef (a quotient of a complex semisimple group by a parabolic subgroup). Its Kähler uniformization corollary considers a compact connected Kähler $X$ with analytically nef tangent bundle and \[ 0\le d=\dim X-\widetilde q(X)\le6,\qquad \widetilde q(X)=\max_{X'\to X\text{ finite étale}}h^1(X',\mathcal O_{X'}). \] It claims a connected finite étale cover whose Albanese morphism is a holomorphically locally trivial bundle with rational homogeneous fiber $F$ of dimension $d$, and \[ \widetilde X\simeq F\times\mathbb C^{\widetilde q(X)}. \] Thus the universal cover is quasi-projective and holomorphically convex, with Remmert reduction to the affine factor. In particular the corollary applies in complex dimension at most six.

Outline of the argument

Manuscript 1 (family 046, 2026-10-05): An arrangement in an arithmetic ball quotient supplies a rank-three lattice-cover obstruction on a simple abelian surface. Compatible local covers and a path criterion show that its infinite cyclic image survives the global relations; the absence of compact analytic fibers then turns failure of Steinness into failure of holomorphic convexity. Manuscript 2 (family 046, 2026-09-23): The construction arranges a connected lift of rational curves with compact components but a noncompact incidence graph, so every holomorphic function is constant on the resulting infinite string. A multiplication cover and weighted Golod--Shafarevich estimates ensure that the relevant graph loop remains infinite after the imposed monodromy relations.

Manuscript 3 (family 058, 2026-09-24): Boundary windows produce compact projective fibers, and bounded plurisubharmonic parameter traces show that intersecting fibers coincide. Functions controlling moving chart boundaries globalize the quotient; inverse-chart compactness makes it a biholomorphism, and special-manifold abelianity controls the remaining deck action. Manuscript 4 (family 058, 2026-09-24): Holomorphic supports and analytic discs select a noncollapsing boundary model despite possible ambient singularities. Joint normal-offset limits and weighted dilation give a quadratic domain; convergence of both maps and inverses identifies the original domain with it, and the homogeneous-domain theorem supplies symmetry.

Manuscript 5 (family 067, 2026-09-25): Known contractions reduce the new case to Picard number one and pseudoindices four or five. The universal minimal-curve family has two smooth fibrations whose projection identities give linear intersection constraints; characteristic-number and integrality comparisons rule out the remaining models and identify the homogeneous possibilities.

Formal verification

Family 046 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

For family 058, the scope page documents the following selections. The selected bounded-domain result allows a singular affine ambient set and nonfree proper cocompact group action, and concludes smoothness and symmetry. It does not select the entire projective universal-cover classification. Manuscript 3 is not among the papers selected by that page, so the family link does not formalize its main conclusion. This entry does not assert that the selected declarations formalize every part of manuscript 4's main conclusion. Comparator files: SymmetricDomains.lean. Declarations: OAI.Release061.main.

Family 067 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources