Iitaka's subadditivity conjecture

Iitaka's subadditivity conjecture asks whether, for a surjective morphism f : X → Y of smooth projective complex varieties with connected fibers and general fiber F, the Kodaira dimensions satisfy κ(X) ≥ κ(F) + κ(Y). Five manuscripts in OpenAI's public mathematics collection, dated 10 to 27 September 2026, claim Campana's orbifold form of the conjecture, from which the logarithmic and ordinary forms follow, together with Popa's variation inequality, a logarithmic additivity theorem and a b-semiampleness theorem. The collection's Lean formalization covers one narrow branch of the additivity theorem.

Background

• As recounted in the main manuscript's introduction:
  • The problem. Iitaka's theories of divisor dimension and logarithmic Kodaira dimension provide the language, and an explicit logarithmic subadditivity conjecture appears in his classification work.
  • Known cases. Kawamata treated curve bases and fibers with good minimal models, Viehweg developed weak positivity and proved addition over a base of general type, and Kollár proved addition for fibers of general type. Birkar treated total dimension at most six, Cao and Păun and Hacon, Popa and Schnell treated abelian and maximal-Albanese-dimension bases, and Cao treated projective klt pairs over surfaces.
  • Logarithmic and orbifold forms. Kovács and Patakfalvi proved the case of log-general-type fibers, Hashizume the case of fibers with abundant log canonical divisor, Maehara and Fujino addition over a base of log general type, Campana addition over an orbifold base of general type, and Wang klt Kähler subadditivity over complex tori. The manuscript also notes earlier preprints of Tsuji and of Maehara that state general ordinary inequalities, and states that neither is an input to its proof.

The original results

• Orbifold subadditivity, 26 September 2026. The main theorem of Orbifold and logarithmic Iitaka subadditivity states that for a smooth compact connected manifold X in Fujiki class 𝒞 with a rational simple normal crossing boundary Δ and a fibration onto a normal compact complex space, the Kodaira dimension of K_X + Δ is no smaller than the sum of the corresponding dimension for a very general fiber and Campana's orbifold base invariant. It describes this as a positive resolution of Campana's orbifold Iitaka conjecture in that formulation, and derives logarithmic subadditivity for smooth quasi-projective varieties and ordinary subadditivity, also over algebraically closed fields of characteristic zero.
• Ordinary subadditivity, 27 September 2026. Projective Hodge lines and ordinary Iitaka subadditivity gives a separate projective proof of κ(X) ≥ κ(F) + κ(Z) over algebraically closed fields of characteristic zero, with F the geometric generic fiber.
• Variation, 26 September 2026. Logarithmic Kodaira dimension and whole-fiber variation states the logarithmic Iitaka–Viehweg inequality, with the variation measured by the field of definition of the whole geometric generic fiber, for projective fibrations of smooth quasi-projective varieties over a base of nonnegative logarithmic Kodaira dimension, and states that this resolves Popa's logarithmic variation conjecture.
• Additivity, 26 September 2026. The reverse logarithmic Kodaira inequality and additivity states the reverse inequality, and with logarithmic subadditivity additivity, for connected-fiber morphisms of smooth projective reduced simple normal crossing pairs whose total space and all boundary strata are smooth over the complement of the base boundary.
• B-semiampleness, 10 September 2026. B-semiampleness for compact log-smooth Kähler fibrations states the compact log-smooth Kähler case of b-semiampleness for fibrations whose log canonical divisor is pulled back from the base.
• Method, as described: a relative Iitaka reduction replaces the fiber by a fibration whose fibers have Kodaira dimension zero; the root of a pluricanonical form on a cyclic cover spans a Hodge line, which gives a boundary and a line bundle on the intermediate base with the same pluricanonical sections; the line bundle is pulled back from a nef line on the image of a period map with an adjoint bigness property, and log-general-type addition and weak positivity then supply the sections.
• Sources. Commit adc7f12 of the openai/math repository: Orbifold and logarithmic Iitaka subadditivity, Projective Hodge lines and ordinary Iitaka subadditivity, Logarithmic Kodaira dimension and whole-fiber variation, The reverse logarithmic Kodaira inequality and additivity and B-semiampleness for compact log-smooth Kähler fibrations.
• Formalization. The scope note states that the Lean development proves the negative-fiber branch of the additivity theorem: for a very general base point, if the logarithmic Kodaira dimension of the fiber is −∞, then so is that of the total space. The other branches of the additivity theorem are outside it, and the subadditivity and variation theorems are not formalized. Comparator statement: LogKodairaFiberNegative.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 31 October 2026; AI Proof Watch row 1 November 2026)
2026-10-08	MathVet, a GitHub review of openai/math, tables at repository commit c76f1e4 of 14 October 2026	Review, fidelity of the formal statement	Rates this family "supporting-only": the challenge covers only the very-general negative-fiber branch of logarithmic additivity, with no orbifold Iitaka statement, no variation inequality and no branch with nonnegative dimension. Among the definitions to check it lists the custom scheme-theoretic framework and the definition of Iitaka dimension, and notes that the conclusion quantifies over fiber models, so that its non-vacuity is not visible from the statement. It records a sandboxed Comparator pass on 8 October 2026.	Review repository. Read on 31 October 2026.
2026-10-10	cert-machine, openai/math lane K, run 38051470892	Verification, two kernels	Records the challenge LogKodairaFiberNegative as certified: Lean's default kernel and the nanoda kernel both accept the solution, in 319 s. C. Toledo's report lists the lane's results.	Repository. The run concerns the formalized statement only.
2026-10-10 to 2026-10-14	con-leche development journal, task #348	Verification, second kernel	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list this family's challenge, so it was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-12	AI Proved What?, episode 033 Do the forms add up?, remade version of 25 October 2026	Reading, exposition	Video explainer of the five preprints, of 55, 40, 75, 51 and 38 pages. It recalls the cases proved by Kawamata, Viehweg, Kollár, Birkar, Cao and Păun, Hacon, Popa and Schnell, and Cao, and the logarithmic and orbifold cases, and states that positive characteristic is not covered and that the additivity statement needs smoothness of the family and its boundary strata over the open base. It also notes that a related result of the collection, on log abundance for compact Kähler spaces, assumes logarithmic Iitaka subadditivity.	Episode status, last checked 30 October 2026: posted as preprints; under expert review, not yet; peer reviewed, not yet; checked in Lean, only one narrow branch; no public assessment by specialists found. The site states that it is made with Anthropic's Claude. Read on 31 October 2026.
2026-10-16	J. Jardine, Lattice24, referee reviews rank_155 of the orbifold manuscript, rank_111 of the projective manuscript, rank_129 of the variation manuscript, rank_157 of the additivity manuscript and rank_196 of the b-semiampleness manuscript, in JJardine919/openai-math-audit	Review, AI-assisted audit	All five reviews report no gap; each lists two or three minor points. These concern cited theorems whose hypotheses the reviewer did not check against the sources, among them results of Brunebarbe and Cadorel, André's monodromy normality, Bakker and Tsimerman's Ax–Schanuel theorem, Fujino's weak positivity for a class-𝒞 source, Campana and Păun's orbifold cotangent theorems and Fujino and Gongyo's b-nefness. The reviews of the variation and additivity manuscripts note that both depend on the logarithmic subadditivity of the orbifold manuscript, and the additivity review states that its upper inequality is proved without it.	Part of the completed Lattice24 audit; the reviews are published under CC BY 4.0.
2026-10-18	AI Proof Watch, record OpenAI reports orbifold Iitaka subadditivity	Catalogue record, assessment	Rates the importance as major, as resolving Campana's orbifold subadditivity conjecture for rational simple-normal-crossing boundary, with ordinary and logarithmic subadditivity as consequences, and the AI involvement as AI-led. It lists as limitations the assumptions of a smooth Fujiki-class-C source, rational boundary, connected fibres and the specified orbifold-base invariant, and notes that earlier general ordinary inequalities were announced in other preprints whose announcements the paper does not use. It rates the technical verification as reported, consistent with the scope note described under Formalization on this page, which does not formalize the subadditivity theorem, and the human understanding as few, the default when no named explanation is documented.	Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.

Notes

• The background summarizes the main manuscript's own account of earlier work.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.