Termination of flips for fourfolds
From OpenAI Aftermath
Termination of flips for fourfolds concerns the termination problem of the minimal model program: whether every sequence of flips and divisorial contractions, chosen at each step among the negative extremal rays, must stop. Five manuscripts in OpenAI's public mathematics collection, dated between 24 September and 7 October 2026, claim termination in dimension four for projective log canonical pairs with rational boundary, and for flip sequences and ordinary programs on compact Kähler fourfolds, which need not be projective. The collection has no Lean formalization of these results.
Background
- As recounted in the introduction of the projective manuscript:
- Existence and termination. Birkar, Cascini, Hacon and McKernan proved the existence of klt flips and of minimal models for klt pairs with big boundary and pseudo-effective adjoint, and Fujino's cone and contraction theorem and Birkar's log canonical flip theorem supply the operations for log canonical pairs. In dimension four, Shokurov's ordered-termination method and Birkar's short proof of the klt case construct minimal models or Mori fibre spaces through selected programs, which does not give termination for every choice of ray.
- The difficulty method. Shokurov introduced a discrepancy-counting difficulty; Kawamata proved termination for terminal fourfolds, and Fujino extended the method to canonical pairs with rational boundary. Alexeev, Hacon and Kawamata proved termination of klt fourfold flips when the negative of the adjoint divisor is numerically equivalent to an effective divisor.
- Recent cases. Chen and Tsakanikas, through generalized pairs, and Moraga give termination for pseudo-effective log canonical fourfolds, and Han, Liu and Zhuang proved termination of every klt fourfold program with big boundary.
The original results
- Projective log canonical fourfolds, 24 September 2026. The main theorem of Termination for projective log canonical fourfolds with rational boundary states that for a projective log canonical pair of dimension four with rational boundary over an algebraically closed field of characteristic zero, with no Q-factoriality or pseudo-effectivity assumed, every negative extremal ray at every stage has its contraction and, when birational, the next model; every permitted program has finitely many birational steps for every sequence of choices, including mixed steps in which a divisorial contraction is followed by a small modification; and every maximal program ends at a log canonical pair with nef adjoint or at a Mori fibre space.
- Compact Kähler fourfolds, 6 and 7 October 2026. Termination of generalized log canonical flips on compact Kähler fourfolds states that every sequence of generalized log canonical flips on a normal globally Weil Q-factorial compact Kähler fourfold terminates, for rational boundary, a fixed nef b-divisor represented on a projective modification, and flips that are projective small diagrams; Termination of generalized-canonical flips on compact Kähler fourfolds treats the generalized canonical case; and Finite ordinary minimal model programs on compact Kähler fourfolds states that every maximal ordinary program starting from a compact Kähler klt fourfold pair with effective rational boundary terminates, at a nef model when the adjoint is pseudo-effective and at a projective Mori fibre space otherwise. The three Kähler manuscripts replaced versions dated 5 October, and the last also replaced a version of 24 September that claimed only that some finite program exists.
- Scope, as stated: the projective theorem is a termination statement, and the semiampleness of a nef endpoint, which needs abundance, is derived in a separate section from other manuscripts of the collection. Its permitted steps exclude flops and extra blowups. The generalized log canonical Kähler theorem concerns flip sequences that exist and does not assert the existence of all contractions or flips. All main theorems require rational coefficients.
- Method, as described: the projective proof follows the difficulty approach. Ranks of cycle classes first remove the steps that lose divisors, and a weighted difficulty on auxiliary terminal models, after Alexeev, Hacon and Kawamata, is shown to drop at each remaining flip. The new ingredient is a branch estimate that controls the normalization branches entering the correction terms when coefficients on the auxiliary models keep decreasing; a transfer argument passes from the complex numbers to every algebraically closed field of characteristic zero.
- Sources. Commit
4eaee87of the openai/math repository: Termination for projective log canonical fourfolds with rational boundary, Termination of generalized log canonical flips on compact Kähler fourfolds, Termination of generalized-canonical flips on compact Kähler fourfolds and Finite ordinary minimal model programs on compact Kähler fourfolds; the earlier versions are kept in the same repository. - Formalization. The collection's Lean library has no scope note or Comparator statement for these manuscripts.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 1 November 2026) |
|---|---|---|---|---|
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_193 (projective), rank_113 (generalized log canonical), rank_312 (generalized canonical), rank_108 and rank_051 (finite ordinary programs, October and September versions) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | All five reviews report no gap and two minor notes each. For the projective manuscript the notes are that Birkar's log canonical theorem is applied to a possibly non-Q-factorial pair without writing out the reduction through a dlt blowup, and that a monodromy argument is terse. For the Kähler manuscripts they concern foundational analytic inputs cited rather than proved, a set of exceptional surfaces not listed in full, and the mutual citation between the finite-program and generalized log canonical manuscripts, in which the reviewer found no circularity, and some steps that are only sketched. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-18 | AI Proof Watch, records Termination for projective log canonical fourfolds with rational boundary and OpenAI reports termination of generalized log canonical Kähler fourfold flips | Catalogue records, assessment | Rates the projective result as major, as settling ordinary termination for the stated projective log canonical fourfold programs, and the generalized log canonical Kähler result as notable, both as AI-led. It lists as limitations that the projective step rules exclude flops, extra blowups and inserted isomorphisms and that nef endpoints need not be abundant, and that the Kähler theorem concerns existing projective small flips under rationality and global Weil Q-factoriality and does not establish the existence of all contractions or flips. It rates the technical verification as reported and the human understanding as few, the defaults when no higher level is documented. | Curated public tracker; both records published 18 October 2026, assessments reviewed 31 October 2026. Read on 1 November 2026. |
| 2026-10-26 | AI Proved What?, episode 056 Can flips go on forever?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of the five preprints. It recalls the known termination cases in dimension four, states that the Kähler flip papers do not claim that every flip exists, that real coefficients, positive characteristic and dimension five and higher are not covered, and that semiampleness of a nef endpoint is not claimed here, and it outlines the difficulty, the branch inequality and why the difficulty must drop. It reports a short script of its own that checks the dimensions of the two exceptional loci of a fourfold flip, a ladder of log discrepancies with its weights, and the rounding inequality behind the branch estimate. | Episode status, last checked 30 October 2026: posted as preprints, with three Kähler manuscripts replaced on 7 October; under expert review, not yet; peer reviewed, not yet; not formalized in Lean; no public assessment by specialists found. The page links an earlier original version without a date. The site states that it is made with Anthropic's Claude. Read on 1 November 2026. |
Notes
- The background summarizes the projective manuscript's own account of earlier work.
- The projective manuscript uses the collection's results on log abundance, see The log abundance conjecture in characteristic zero, and on bounded complements and uniform Cartier sections only for consequences at the endpoints, and states that its termination proof does not depend on them.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
