Algebraic and complex geometry · Result 066

Bounded klt complements for Fano contractions

2 papersLean

Proves the finite-rational-coefficient form of Shokurov’s bounded-klt-complement conjecture for ϵ-lc complex Fano-type pairs with nef anti-log-canonical divisor. For ϵ-lc Fano contractions over any algebraically closed characteristic-zero field, it gives klt complements near every base point, with index bounded only by dimension and positive rational ϵ.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Bounded klt complements for Fano contractions

OpenAI · September 25, 2026

For fixed dimension d and positive rational ϵ, we prove that every ϵ-log-canonical Fano contraction over an algebraically closed field of characteristic zero admits, near each closed base point, a klt complement of index bounded only by d and ϵ. Over ℂ, we also obtain monotone klt complements for Fano type pairs with nef anti-log-canonical divisor and coefficients in a fixed finite rational set. This proves the finite-rational-coefficient form of Shokurov's bounded-klt-complement conjecture.

Read PDF Download Source

Cite

@misc{OAI:Bounded-klt-complements-for-Fano-contractions-September-25-2026,
  author = {{OpenAI}},
  title = {{Bounded klt complements for Fano contractions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Bounded-klt-complements-for-Fano-contractions-September-25-2026/Bounded-klt-complements-for-Fano-contractions-September-25-2026.pdf}{OAI:Bounded-klt-complements-for-Fano-contractions-September-25-2026}},
  year = {2026}
}

Uniform Cartier sections for Fano type contractions

OpenAI · September 25, 2026

We prove the Cartier-divisor conjecture of Birkar and Shokurov for rational boundaries in characteristic zero and for real boundaries over ℂ. For an ϵ-lc Fano type contraction with positive-dimensional base and nef negative log canonical class, a Cartier divisor through any prescribed base point can be chosen with pullback log canonical threshold bounded below in terms of the dimension and ϵ alone.

Read PDF Download Source

Cite

@misc{OAI:Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026,
  author = {{OpenAI}},
  title = {{Uniform Cartier sections for Fano type contractions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026.pdf}{OAI:Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Uniform Cartier sections for Fano type contractions

Scope

The paper develops uniform Cartier sections for Fano-type contractions as a step toward bounded klt complements. The linked formalization proves a local compactness result: for positive numbers \(a_i\), the chart-field retractions indexed by nonnegative weights satisfying \(\sum_i a_iw_i=1\) form a compact set in the pointwise topology on the fraction field.

The chart is built over an algebraically closed field from the localization of a polynomial ring at its origin. Its local domain is Noetherian, essentially of finite type and formally unramified over that localization, and formally étale over the polynomial ring. Uniform Cartier sections, bounded klt complements, and the paper's real-boundary and companion conclusions are outside this supporting statement.

Comparator links

Result	Comparator statement
Compactness of normalized chart-field retractions	CartierChartCompactnessSupport.lean

Scope note on GitHub →