Anticanonical nonvanishing from smooth semipositivity
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
For every smooth connected projective complex X, if $-K_X$ admits a smooth Hermitian metric with semipositive Chern curvature, must $H^{0}(X,-mK_X)\neq 0$ for some positive integer m?Short English statement
For every smooth connected projective complex X, if $-K_X$ admits a smooth Hermitian metric with semipositive Chern curvature, must $H^{0}(X,-mK_X)\neq 0$ for some positive integer m?Sources
- S1 Original question source or mathematical context. https://doi.org/10.1007/s40574-020-00250-9.
- S2 Original question source or mathematical context. https://doi.org/10.4171/owr/2006/40.
- S3 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Anticanonical-nonvanishing-from-smooth-semipositivity-September-26-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2585
Manuscript 1 (family 068, 2026-09-26): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.
Anticanonical nonvanishing from smooth semipositivity
OpenAI's claim
Smooth semipositivity of the anticanonical bundle is claimed to force a positive-degree anticanonical section on every smooth complex projective variety. The cited manuscript argues for that result; its relation to this problem is specified below.Mathematical statement of the claimed result
Mathematical claim 1.
For every smooth connected projective complex variety $X$ whose anticanonical line has a smooth Hermitian metric with nonnegative Chern curvature, OpenAI claims \[ \exists m\in\mathbb Z_{>0}:\quad H^0(X,\mathcal O_X(-mK_X))\ne0. \] No Euler-characteristic or rational-connectedness assumption occurs in this headline theorem. Smooth semipositivity is stronger than an assumed nef numerical class.Outline of the argument
Manuscript 1 (family 068, 2026-09-26): Section ratios define a rational base on which the generic relative adjoint spaces stay one-dimensional. Bergman positivity transfers the specified line, while compact-monodromy structure requires an invariant section on the remaining factor; multiplication with the flat canonical frames and a finite étale norm descend the resulting section.Formal verification
Family 068 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
- OpenAI, Anticanonical nonvanishing from smooth semipositivity, 2026-09-26; citation key
OAI:Anticanonical-nonvanishing-from-smooth-semipositivity-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:headline. - OpenAI catalogue entry.