View source for Shokurov's conjecture on bounded klt complements

'''Shokurov's conjecture on bounded klt complements''' asks whether, for Fano contractions of a fixed dimension whose singularities have log discrepancies bounded below by a fixed ''ε'' > 0, one index ''N'' suffices for klt complements near every point of the base. Two manuscripts in OpenAI's public mathematics collection, both dated 25 September 2026, claim it by independent routes: one constructs bounded klt complements directly, and its companion proves the equivalent Cartier-section form of Birkar and Shokurov. The collection's Lean formalization covers one supporting compactness lemma of the companion paper, not the main theorems.

== Background ==
* As recounted in the manuscripts' introductions:
** ''Complements.'' Shokurov introduced complements in his work on threefold log flips and formulated their boundedness in his theory of surfaces; Prokhorov and Shokurov developed the passage from global to local complements and an inductive program in higher dimension. A complement near a point of the base is an effective boundary ''B'' for which ''N''(''K''<sub>''X''</sub> + ''B'') is Cartier and linearly trivial there, and a klt complement must keep every log discrepancy positive.
** ''Known cases.'' Birkar proved boundedness of lc complements for Fano type fibrations with hyperstandard coefficients, and bounded klt complements for boundary-free Fano fibrations over curves. Chen showed that bounded klt complements are equivalent to a uniform lower bound for local thresholds of Cartier divisors pulled back from the base, and proved both for bases of dimension at most two.
** ''Cartier sections.'' Sankaran and Santos treated the weighted-blowup case of Birkar's question, Ambro constructed invariant Cartier sections in the toric setting, and Chen removed the coefficient restriction in the toric case.

== The original results ==
* '''Bounded klt complements, 25 September 2026.''' The main theorem of ''Bounded klt complements for Fano contractions'' states that for every dimension ''d'' and rational ''ε'' > 0 there is an integer ''N'', depending only on ''d'' and ''ε'', such that every projective contraction ''f'' : ''X'' → ''Z'' of normal varieties over an algebraically closed field of characteristic zero, with ''X'' of dimension ''d'' and ''ε''-lc, ''K''<sub>''X''</sub> rationally Cartier and −''K''<sub>''X''</sub> ample over ''Z'', has near every closed point of ''Z'' an effective boundary ''B'' with the pair klt and ''N''(''K''<sub>''X''</sub> + ''B'') an integral Cartier divisor linearly equivalent to zero. A corollary gives, over the complex numbers, the finite-rational-coefficient form of Shokurov's bounded klt complement conjecture as stated by Chen.
* '''Uniform Cartier sections, 25 September 2026.''' The main theorem of ''Uniform Cartier sections for Fano type contractions'' states that for every ''d'' and ''ε'' > 0 there is ''τ'' > 0, depending only on ''d'' and ''ε'', such that for every ''ε''-lc rational pair of dimension ''d'' and every Fano type contraction to a positive-dimensional quasi-projective base with −''K''<sub>''X''</sub> − ''B'' nef over the base, each closed point of the base lies on a nonzero effective Cartier divisor ''D'' on a neighbourhood for which the pair with boundary ''B'' + ''τ'' ''f''<sup>*</sup>''D'' is log canonical. Through Chen's equivalence it states that this resolves the rational-boundary conjecture, with a corollary for real boundaries over the complex numbers. Its new input is a theorem on bounded klt complements for birational Fano type contractions. Each manuscript describes the other as an independent companion.
* ''Scope, as stated:'' the complements are klt, not ''ε''-lc; the stronger requirement recorded by Chen is not asserted. The coefficient version requires a finite set of rational coefficients. The index and the threshold depend only on ''d'' and ''ε'' and are not effective.
* ''Method, as described:'' the first manuscript reduces, through Chen's equivalence, to a uniform lower bound for the log canonical threshold of the pulled-back maximal ideal in the birational case without boundary, and argues by contradiction. Anticanonical sections are encoded in an affine cone, normalized volume is minimized under a log canonical constraint after an exact-penalization step, and stable degeneration with a torus of maximal rank gives a graded model with a weak essentiality property; trace estimates based on Takagi's comparison of multiplier and test ideals finish the argument. The companion manuscript turns a failing sequence, with bounded lc complements, into klt germs with cyclic group actions and derives a contradiction from a character and pinning argument for quasi-monomial valuations.
* '''Sources.''' Commit <code>adc7f12</code> of the openai/math repository: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Bounded-klt-complements-for-Fano-contractions-September-25-2026 ''Bounded klt complements for Fano contractions''] and [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026 ''Uniform Cartier sections for Fano type contractions''].
* '''Formalization.''' The [https://github.com/openai/math/blob/4eaee87548250b2682affda7d05d947c05554bae/lean/docs/066.md scope note], added to the repository on 8 October 2026 and revised on 26 October 2026, links the companion paper. It states that the Lean development proves a local compactness result: for positive numbers ''a''<sub>''i''</sub>, the chart-field retractions indexed by nonnegative weights with weighted sum one form a compact set in the pointwise topology on the fraction field, for one chart over an algebraically closed field. It states that this does not construct the Cartier divisor with the uniform threshold bound, and that bounded klt complements and the paper's real-boundary and companion conclusions are outside the comparison. Comparator statement: [https://github.com/openai/math/blob/4eaee87548250b2682affda7d05d947c05554bae/lean/ComparatorChallenges/CartierChartCompactnessSupport.lean <code>CartierChartCompactnessSupport.lean</code>].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 1 November 2026; AI Proof Watch row 1 November 2026)
|-
| 2026-10-10 || [https://github.com/mathvet/mathvet MathVet], a GitHub review of openai/math, tables at repository commit <code>c76f1e4</code> of 14 October 2026 || Review, fidelity of the formal statement || Rates this family "supporting-only": the Lean states only a topological compactness lemma for monomial valuations on one chart, an auxiliary step of the companion Cartier paper, and says nothing about klt complements, Fano type contractions, indices or Shokurov's conjecture; it notes that the linked paper is the companion rather than the headline paper. Among the definitions to check it lists the solver-defined chart-field retraction and weight set, and it judges the chart hypotheses satisfiable, so the statement is not vacuous. It records a sandboxed Comparator pass on 10 October 2026, with about 1,600 lines in the dependency cone. || Review repository. Read on 1 November 2026.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/e35cd57a5fbd5b870c66d88697297a33f64f0eb2/certs/openai-math-kernel.json cert-machine], openai/math lane K, run 38017370880 || Verification, two kernels || Records the challenge <code>CartierChartCompactnessSupport</code> as certified: Lean's default kernel and the nanoda kernel both accept the solution, in 158 s. C. Toledo's [https://carlostoledo.co/reports/openai-math.html report] lists the lane's results. || Repository. The run concerns the formalized statement only.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal], task #348 || Verification, second kernel || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, 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 || M. Bintz, [https://bsky.app/profile/spurious-bows.bsky.social/post/3mxpl2opuvs2i thread on recurring techniques in the release], [https://bsky.app/profile/spurious-bows.bsky.social/post/3mxpl2oqx3k2i third pair] || Reading, comparison of techniques || A thread on techniques that recur across manuscripts of the collection without cross-citation, with the equality sign used loosely. Its third pair matches the manuscript ''Minimal models and Mori fibre spaces for generalized log canonical '''Q'''-pairs'', on the page [[The generalised abundance conjecture]], with ''Bounded klt complements for Fano contractions'': Lemma 8.3 of the first with Proposition 14.3 of the second, and broadly Lemma 6.3 to Section 8.3 of the first with Lemma 11.6 to Proposition 14.5 of the second. It suggests that the shared ideas may come from the proof systems sharing a workspace. || Social media thread on Bluesky. Read on 31 October 2026.
|-
| 2026-10-13 || ''AI Proved What?'', episode 066 [https://aiprovedwhat.com/episodes/066-bounded-klt-complements-fano-contractions/ A bounded index?], remade version of 26 October 2026 || Reading, exposition || Video explainer of the two preprints, of 93 and 106 pages. It recalls Shokurov's complements, Birkar's bounded lc complements, the cones over rational normal curves that show why ''ε'' must be fixed, and Chen's reduction and his proof for bases of dimension at most two. It states that the complements are klt rather than ''ε''-lc, that the coefficient version needs a finite set of rational coefficients, and that the two papers reach the equivalent conjectures by independent routes; it notes that the Cartier paper adapts two lemmas from the collection's paper on [[The ordinary double point volume gap]]. || Episode status, last checked 30 October 2026: posted as preprints, released 6 October, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, main theorems no, the catalogued check covers one supporting compactness lemma of the companion paper and ten uncatalogued files add more of its local algebra, which the site did not run; no public assessment by specialists found. A correction of 15 October concerns these uncatalogued files. The site states that it is made with Anthropic's Claude. Read on 1 November 2026.
|-
| 2026-10-16 || J. Jardine, Lattice24, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_158.json referee review rank_158] of ''Bounded klt complements for Fano contractions'', in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] || Review, AI-assisted audit || Reports no gap, with one minor point: the finite-coefficient corollary uses Chen's equivalence with zero boundary, which suffices only if Chen's theorem derives the coefficient version from the zero-boundary one; the reviewer could not access Chen's theorem text, so this is a dependency to verify, not a demonstrated error. It states that about half of the technical middle of a proof of roughly 7,800 lines was not verified line by line, so the no-gap verdict carries low confidence there. The audit's results index lists no review of the companion manuscript. || Part of the completed Lattice24 audit; the reviews are published under CC BY 4.0.
|-
| 2026-10-18 || ''AI Proof Watch'', record [https://aiproofwatch.com/updates/openai-reports-bounded-klt-complements-for-fano-contractions-3a262b76 OpenAI reports bounded klt complements for Fano contractions] || Catalogue record, assessment || Rates the importance as major, as a broad bounded klt complement theorem that implies the finite-rational-coefficient form of Shokurov's conjecture, and the AI involvement as AI-led. It lists as limitations the assumptions of ''ε''-log-canonical singularities, characteristic zero, fixed dimension and a Fano contraction, and that the complement exists only locally near each closed base point, not globally over the base. It rates the technical verification as reported and the human understanding as few, the defaults when no higher level is documented, consistent with the Formalization section on this page, which lists only a supporting compactness result in Lean. || Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.
|}

== Notes ==
* The background summarizes the manuscripts' 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.

[[Category:OpenAI results]]