we-solve (beta)

Math-2544-A1 · revision r1 · on Math-2544

OpenAI claim summary for Math-2544

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

Manuscript 1 (family 056, 2026-09-24): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Existence of a finite ordinary Kähler fourfold program
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Existence of a finite ordinary Kähler fourfold program

OpenAI's claim

For the stated compact Kähler klt fourfold pairs, at least one ordinary program is claimed to start on the supplied model, take finitely many steps, and finish nef or in a Mori fiber space. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
For a normal globally Weil rational-factorial compact Kähler fourfold $X$ with rational effective $\Delta$ and klt pair $(X,\Delta)$, OpenAI claims existence of a finite ordinary negative-extremal-ray program starting on $X$, using projective divisorial contractions and flips. With $D=K_X+\Delta$, its endpoint satisfies \[ D\text{ pseudo-effective}\Rightarrow D_n\text{ nef},\qquad D\text{ not pseudo-effective}\Rightarrow X_n\to S\text{ a Mori fiber contraction}. \] All models remain normal globally Weil rational-factorial compact Kähler and klt. The first composite extracts no divisor and increases discrepancies weakly for all primes and strictly for contracted original primes. The Mori contraction has connected fibers, normal compact Kähler base of dimension below four, relative Picard rank one and relatively ample $-D_n$. Each contraction has relative Bott--Chern dimension one; strong rational-factoriality is preserved when assumed. Unlike the later manuscript, this main theorem states existence of a finite program, not termination of every choice.

Outline of the argument

Manuscript 1 (family 056, 2026-09-24): A single initial Kähler form is tracked as a positive current on the comparison models. Real-boundary terminal termination and power-free descent of actual lines preserve a fixed positive intersection gap, so rational perturbations transfer an auxiliary construction into the required ordinary program.

Formal verification

Family 056 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