OpenAI claim summary for Math-2530

Rank-preserving contraction for anticanonical fibrations

OpenAI's claim

The paper claims unweighted integrable anticanonical metric descent with an explicit exceptional correction, together with boundary-pole transfer and rank-preserving contractions under the stated hypotheses. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

Let $X$ be smooth connected projective complex with $H^0(X,\Omega_X^q)=0$ for $q>0$ and smoothly semipositive $L=-K_X$. Equip an algebraic torus action by $T$ with the differential linearization on the anticanonical bundle. Take a dominant $T$-invariant rational $f:X\dashrightarrow Z$ to smooth connected projective $Z$, with $\mathbb C(Z)$ relatively algebraically closed in $\mathbb C(X)$. On a resolution $\pi:Y\to X$, $f_Y:Y\to Z$, put $L_Y=\pi^*L$, $E_Y=K_{Y/X}$ and $\eta=\operatorname{Spec}\mathbb C(Z)$. Assume \[ H^0(Y_\eta,pL_Y)^T\ne0\text{ for some }p>0,\qquad \dim_{\mathbb C(Z)}H^0(Y_\eta,E_Y+mL_Y)^T=1\text{ for every }m\in a\mathbb Z_{>0} \] for some $a>0$. OpenAI claims either a global invariant section $H^0(X,rL)^T\ne0$ for some $r>0$, or a dominant rational $Z\dashrightarrow W$ to a smooth connected projective $W$ with $\dim W<\dim Z$ and relatively algebraically closed $\mathbb C(W)\subset\mathbb C(X)$, such that the composite again satisfies these two generic-fiber conditions, with possibly different positive indices.

Outline of the argument

Manuscript 1 (family 068, 2026-09-26): A normal equidimensional toroidal model compares Jacobian orders with divisor pullback multiplicities to determine the base correction. Every divisorial valuation is checked, including boundary intersections; two-metric estimates then retain finite volume and the exact generic adjoint rank needed to contract an invariant fibration or produce a 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, Metric descent and rank-preserving contractions, 2026-09-26; citation key OAI:Metric-descent-and-rank-preserving-contractions-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: g:cf:contraction-theorem.
• OpenAI catalogue entry.