OpenAI claim summary for Math-2562

Logarithmic Kodaira additivity under stratum smoothness

OpenAI's claim

For reduced normal-crossing projective pairs that are smooth on every boundary stratum over the open base, OpenAI claims logarithmic Kodaira additivity, including the cases with negative-infinite dimension. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

Take a connected-fiber surjective morphism $f:X\to Y$ of smooth connected projective complex varieties, reduced simple-normal-crossing divisors $E,D$ with $\operatorname{Supp}(f^*D)\subseteq\operatorname{Supp}E$, and $V=Y\setminus D$. Require $X$ and each nonempty boundary intersection stratum of $E$, restricted over $V$, to be smooth over $V$. For a very general fiber $F$ and $E_F=E|_F$, OpenAI claims \[ \kappa(X,K_X+E)=\kappa(Y,K_Y+D)+\kappa(F,K_F+E_F). \] The independent main theorem proves the upper inequality; equality uses the companion logarithmic subadditivity result. The zero divisors and $-\infty$ Kodaira dimensions are included. Smoothness is required over the original open base, with no assertion of smoothness above $D$.

Outline of the argument

Manuscript 1 (family 033, 2026-09-26): Iterated logarithmic cotangent and Higgs maps turn a selected pluriform into base sections with controlled coefficients. Period-image positivity and a canonical bundle formula supply the reverse inequality; combining it with subadditivity yields equality under the stated stratum-smoothness assumptions.

Formal verification

For family 033, the scope page documents the following selections. Only the case of a negative-infinite logarithmic fiber dimension is selected; it forces negative-infinite dimension upstairs and vanishing of positive pluriforms. Finite-dimensional fibers and the negative-base case remain outside the linked statement. This entry does not assert that the selected declarations formalize every part of manuscript 1's main conclusion. Comparator files: LogKodairaFiberNegative.lean. Declarations: OAI.ReverseLogKodaira.SmoothProjectiveVariety.veryGenerally_fiber_negative_branch.

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, The reverse logarithmic Kodaira inequality and additivity, 2026-09-26; citation key OAI:The-reverse-logarithmic-Kodaira-inequality-and-additivity-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: cor:additivity.
• Family 033: Lean scope.
• Comparator LogKodairaFiberNegative.json.
• Comparator LogKodairaFiberNegative.lean.
• OpenAI catalogue entry.