Talagrand’s expectation thresholds, discrete convexity, and graph decompositions
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves that integral and fractional expectation thresholds differ by at most a universal factor, and resolves Talagrand’s discrete-convexity conjecture. An application proves the Ascoli–He–Park–Talagrand graph-decomposition conjecture: every graph’s edges split into a universally bounded number of fixed pieces, each with containment threshold at most a universal constant times the original graph’s integral expectation threshold. The pieces’ embeddings need not agree on shared vertices. (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 only part of the result described above, or a narrower statement.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
Three other possible matches are listed below the card, among them Theorem 1.1 in Integral and fractional expectation thresholds are equivalent and Corollary 1.2(Two unions at constant density loss) in Talagrand’s discrete-convexity conjecture.
There exist an absolute integer k\geq2 and an absolute constant L\geq1 such that, for every n\geq2 and every graph H on at most n vertices, the edges of H admit a partition
We prove the graph-decomposition conjecture of Ascoli, He, Park, and Talagrand. Every graph admits a partition into a universally bounded number of fixed edge pieces, each having ordinary containment threshold at most a universal constant times the original graph’s integral expectation threshold. The partition is chosen before sampling the random host, and the separate embeddings of the pieces need not agree on shared vertices.
We prove Talagrand’s conjecture that integral and fractional expectation thresholds are within a universal constant factor, with the same covering budget.
We prove Talagrand’s discrete-convexity conjecture. There is a universal integer k such that, whenever an arbitrary family has Bernoulli product measure at least \(1-1/k\), the sets not contained in a union of k members admit a cover of total cost at most 1/2 at the same density.
Two Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
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.
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”.
For every finite nonempty X and every nonempty proper increasing family \F\subseteq2^X,
q_f(\F)\le25\cdot512^4\,q(\F).
Both thresholds use the budget 1/2. The constant is independent of |X|, the sizes of the minimal members of \F, and the support of the fractional cover.
The words they share: increasing, fractional, thresholds, cover, nonempty, 1/2, family, integral, expectation, budget, proper, finite.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
TalagrandExpectationThreshold.lean, the release lists it as a main result.
theoremtalagrand_expectation_threshold_equivalence [Nonempty α] (F : Family α) (_hF : F.Nonempty) (hproper : F ≠ Finset.univ) (hIncreasing : Increasing F) : qf F ≤ ((25 : ℝ) * (512 : ℝ) ^ 4) * q F := bysorry
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”.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
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 part of the advertised result (their term: “partial”).
Their note:Two of the three claims are stated with explicit constants: talagrand_expectation_threshold_equivalence : qf F ≤ (25 * 512^4) * q F (increasing nonempty proper F) and talagrand_discrete_convexity with k = 2^75 (Small p (exceptional (2^75) D) from 1 - 1/2^75 ≤ familyMeasure p D). The summary’s application, the Ascoli-He-Park-Talagrand graph-decomposition conjecture (also in the family title), has no challenge statement and the docs do not mention it.
“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.
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.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name:The Ascoli–He–Park–Talagrand graph-decomposition theorem (October-5 manuscript, not linked by the scope note).
“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Talagrand’s expectation-threshold conjecture asks whether the fractional and integral expectation thresholds are comparable by an absolute constant. The formalized result proves $q_f(\mathcal F)\le25\cdot512^4 q(\mathcal F)$ for every nonempty proper increasing family on a finite nonempty ground set. Both thresholds use cover budget $1/2$, and fractional covers may assign weights to every subset, including the empty set.
The formalized result proves Talagrand’s discrete-convexity assertion with $k=2^{75}$. If a family of subsets of a finite nonempty ground set has Bernoulli-$p$ measure at least $1-1/k$, then the sets not contained in a union of $k$ members form a $p$-small family: they have a containment cover of total $p$-cost at most $1/2$. This holds for every $0<p<1$, with repeated members allowed in the union and no monotonicity assumption.
AI-drafted comparisons, with no recorded human review
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the convexity paper with k = 2^75: a family of Bernoulli-p measure at least 1 − 1/k leaves a p-small family of sets not covered by a union of k members. The two-union corollary is not part of the statement.
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem with its constant: q_f(F) ≤ 25·512⁴·q(F) for every nonempty proper increasing family.
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.
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.
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.
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 “Major math journal”. The page says that nothing on it is verified.
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
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 175The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Compare the proposed paper and Lean matches
Family 175Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing.Open the form
Why this passage is shown
Theorem 1.1
In Graph Decompositions at the Integral Expectation Threshold, 5 October 2026
How it was found
Its words were compared with the words of OpenAI’s catalogue description.
Only a special case is stated, or a co-equal headline claim has no challenge statement.
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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator with Lean’s kernel: accepted (the check took 29 s; peak memory 2.1 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator with Lean’s kernel: accepted (the check took 68 s; peak memory 2.1 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.