Popa's logarithmic additivity conjecture for log-smooth families
For smooth families, subadditivity of Kodaira dimension is expected to become equality. Popa (Conjecture 3.9 of Conjectures on the Kodaira dimension) asked: let be an algebraic fibre space between smooth projective varieties, an SNC divisor on and an SNC divisor on with , and assume is log-smooth over (each stratum of , including , is smooth over ). For a general fibre over , is ? It generalises his Conjecture 3.1 for smooth projective fibre spaces of quasi-projective varieties, known when the base is of log general type, a curve, or compactifies to an abelian variety, or when has semiample canonical bundle.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Birational geometry, Kodaira dimension of smooth families
- Posed by
- Mihnea Popa, Conjectures on the Kodaira dimension, Conjecture 3.9 and footnote 5 (author version 13 June 2023; LMS Lecture Note Series 489, 2025)
- Year posed
- 2023
- Years open
- 3y
- Solved
- 2026-09-26
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 35 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: under Popa's hypotheses (reduced SNC , , support inclusion, stratum smoothness over ), , and if either term on the right is every vanishes; no abundance or good-model hypothesis. With the family's logarithmic subadditivity this gives equality, Corollary 1.2. Either divisor may be zero, which covers additivity for smooth projective morphisms; the paper itself claims only Conjecture 3.9. Not covered: families that are not log-smooth over the open base.
What the AI did
Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems. The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this family is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscripts are authored as OpenAI with no human author named. The README also cautions that unformalized results could have issues. The upper inequality is proved independently; the equality uses the logarithmic subadditivity corollary of the family's orbifold paper. Only the negative-fibre branch is formalized in Lean (see the verification note).
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 and Corollary 1.2 of 'The reverse logarithmic Kodaira inequality and additivity', read against Popa's Conjecture 3.9 and footnote 5 in his 13 June 2023 author version (fetched and read here); the hypotheses match. The proof was not refereed. Lean: lean/ComparatorChallenges/LogKodairaFiberNegative.json exists with solution_module OAI.AlgebraicGeometry.LogKodaira.FiberNegative (present at the pinned commit) but the challenge is not in the formalization catalogue. Its statement was read: for a very general base point, if the fibre's log Kodaira dimension is -infinity then the total one is -infinity and every positive-degree log pluriform vanishes. That is only the elementary negative-fibre branch, not the headline, so the entry is Unreviewed rather than Lean-checked. Not rebuilt here. The equality depends on the family's unreviewed subadditivity paper.