Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Bounded klt complements for Fano contractions

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

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 ϵ. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express a supporting step or a different result. Read the assessments

What the papers state

Theorem 1.1

In Bounded klt complements for Fano contractions, 25 September 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

For every positive integer d and positive rational number \epsilon there is a positive integer N=N(d,\epsilon) with the following property. Let k be an algebraically closed field of characteristic zero, and let f\colon X\to Z be a projective surjective morphism of normal integral k-varieties such that f_*\OO_X=\OO_Z, \dim X=d, K_X is \Q-Cartier, X is \epsilon-lc, and -K_X is ample over Z. For every closed point z\in Z there are an effective \Q-divisor B on X and a Zariski open neighbourhood U of z such that (X,B) is klt over U and

N(K_X+B)|_{f^{-1}(U)}\sim 0

is an integral Cartier divisor.

No Lean statement in the release is paired with this theorem.

Corollary 1.2

In Bounded klt complements for Fano contractions, 25 September 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

Fix a positive integer d, a real number \epsilon>0, and a finite set I\subset[0,1]\cap\Q. There is a positive integer M=M(d,\epsilon,I) with the following property. Let (X,\Delta) be an \epsilon-lc pair of dimension d with coefficients in I, over \C. Let f\colon X\to Z be a contraction of quasi-projective normal varieties, assume that X is of Fano type over Z, and assume that -(K_X+\Delta) is nef over Z. For every closed z\in Z, there is an effective \Q-divisor \Delta^+\ge\Delta such that, near f^{-1}(z), the pair (X,\Delta^+) is klt and M(K_X+\Delta^+) is Cartier and linearly trivial after shrinking the base about z.

No Lean statement in the release is paired with this theorem.

The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.

Three more possible matches

  • Theorem 1 (Uniform Cartier sections) in Uniform Cartier sections for Fano type contractions, 25 September 2026.
  • Theorem 2 (Birational klt complements) in Uniform Cartier sections for Fano type contractions, 25 September 2026.
  • Corollary 3 (Real boundaries) in Uniform Cartier sections for Fano type contractions, 25 September 2026.
Reported proof verification
One Lean statement in the release; three independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Two current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Bounded klt complements for Fano contractions

25 September 2026, current edition.

Read it herePDF

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.

Uniform Cartier sections for Fano type contractions

25 September 2026, current edition.

Read it herePDF

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.

One Lean statement in this family

Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

CartierChartCompactnessSupport

The paper states

Theorem 1 (Uniform Cartier sections)

In Uniform Cartier sections for Fano type contractions, 25 September 2026

For every integer d>0 and every real number \epsilon>0, there is a real number \tau=\tau(d,\epsilon)>0 with the following property. Let (X,B) be an \epsilon-lc rational pair of dimension d, and let f:X\to Z be a Fano type contraction of normal integral quasi-projective varieties with \dim Z>0. Suppose that -(K_X+B) is nef over Z. For every closed point z\in Z, there are an open neighbourhood U of z and a nonzero effective Cartier divisor D on U, with z\in\Supp D, such that

\bigl(f^{-1}(U),B|_{f^{-1}(U)}+\tau f^*D\bigr) \quad\text{is log canonical.}

The words they share: cartier, closed, fano, real, sections, type, uniform.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Compactness of normalized chart-field retractions

CartierChartCompactnessSupport.lean, the release lists it as a main result.

lemma isCompact_closedChartFieldRetraction_cone    (a : σ → NNReal) (ha : ∀ i, 0 < a i) :    IsCompact ((fun w : σ → NNReal => fun x : K =>      closedChartFieldRetraction (σ := σ) (k := k) (R := R) (A := A) w x) ''      normalizedWeights a) := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express a supporting result (their term: “supporting-only”).

Their note: The Lean states only a topological compactness lemma: for k algebraically closed, a closed etale chart A with fraction field K (hypotheses in the variable block) and positive reals a_i, the monomial valuations K -> WithTop ℝ of weights w >= 0 with sum a_i w_i = 1 form a compact subset of K -> WithTop ℝ in the pointwise topology. It is an auxiliary step (cf. Lemma E.2 of the companion Uniform Cartier sections paper); nothing about klt complements, Fano type pairs or contractions, indices, or Shokurov’s conjecture is stated, and the linked paper is the companion Cartier paper rather than the headline paper.

Definitions the group asks readers to compare with the paper: closedChartFieldRetraction: solver-defined (OAI.CartierSections) AddValuation K (WithTop ℝ): v_w(a/b) = val_w(theta a) - val_w(theta b) for theta = closedChartExpansion : A ->alg[k] k[[x_sigma]] (formal coordinate expansion of the completed local ring, injective by faithful flatness) and val_w(f) = inf over the support of f of sum w_i d_i; zero weights allowed; part of the statement; normalizedWeights a: solver-defined set {w : sigma -> NNReal | sum a_i * w_i = 1}, a compact simplex when every a_i > 0; typeclass block on A: local Noetherian domain, essentially of finite type and formally unramified over R = k[x_sigma] localised at the origin ideal idealOfVars, formally etale over k[x_sigma], with K = Frac A, k algebraically closed and sigma a Fintype: encodes a ‘closed etale chart’; appears satisfiable (e.g. A = R, a localisation of k[x_sigma] and hence formally etale over it), so the statement is not vacuous; note FormallyEtale, not Etale; topology: IsCompact in the Pi (pointwise-evaluation) topology on K -> WithTop ℝ, WithTop ℝ carrying the order topology (top = +infinity); standard Mathlib; local instance polynomialOrigin_isMaximal_topology: re-exports a proved fact that idealOfVars is a maximal ideal; no assumption; the challenge file imports OAI.AlgebraicGeometry.CartierSections.FieldTopology and FieldRetraction, so the definitions above are solver-authored rather than Mathlib-only

“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a supporting result (their term: “SUPPORT-ONLY”).

The gap they name: The whole headline. The challenge proves only that, on a closed étale chart (local Noetherian domain A, essentially of finite type and formally unramified over the localization R of k[σ] at the origin, formally étale over k[σ], k algebraically closed), the family of chart-field retraction valuations K → WithTop ℝ indexed by weights w ≥ 0 with Σ aᵢwᵢ = 1 (all aᵢ > 0) is compact in the pointwise topology.

“SUPPORT-ONLY”, in their words: The challenge statements state only supporting results.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

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.

AI-drafted comparisons, with no recorded human review

  • Compactness of normalized chart-field retractions CartierChartCompactnessSupport

    Unreviewed AI draft: states a supporting result. States a local compactness lemma about chart-field retractions used towards uniform Cartier sections, one of the five supporting comparisons named in the Comparator README. Uniform Cartier sections and bounded complements are outside it.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Compactness of normalized chart-field retractions CartierChartCompactnessSupport

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.10 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 123 s; peak memory 3.4 GiB).10 October 2026Original report

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “A strong professor’s paper of the year”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 066 No single paper statement clearly matches OpenAI’s description by wording, and no review identifying the intended theorem is recorded. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 066 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form