we-solve (beta)

Math-2491-A1 · revision r1 · on Math-2491

OpenAI claim summary for Math-2491

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 at unsolvedmath.com: 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.

The claimed estimate uses $1+\log_2 e(H)$, which is bounded by a universal multiple of $\log|V(H)|$ for every graph with an edge. It therefore implies the requested graph-expectation-threshold bound with one universal constant; edgeless graphs are contained trivially.

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

Manuscript

Contents
  1. The Graphic Kahn–Kalai Conjecture
  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

The Graphic Kahn–Kalai Conjecture

OpenAI's claim

The second Kahn--Kalai bound: The claimed graph containment threshold is at most $C p_{\mathrm E}(n,H)(1+\log_2 |E(H)|)$ for every nonempty graph $H$ fitting inside the host vertex set. The constant is universal.

Mathematical statement of the claimed result

Mathematical claim 1.
For a finite simple $H$ with $h=e(H)\ge1$ and at most $n\ge2$ vertices, let $p_c(n,H)=\inf\{p:\mathbb P(G(n,p)\supset H)\ge1/2\}$ and $p_E(n,H)=\inf\{p:\mathbb E N(G(n,p),F)\ge1/2\text{ for every }F\subseteq H\}$, where $N$ counts noninduced copies. The claimed edge-dependent bound is \[p_c(n,H)\le\min\{1,\,2048e^{50}p_E(n,H)(1+\log_2h)\}.\] It implies $p_c(n,H)\le6144e^{50}p_E(n,H)\log_2n$. Since $h\le\binom{|V(H)|}{2}$, the stronger edge-dependent statement also supplies one universal constant times $p_E(n,H)\log|V(H)|$.

Outline of the argument

The second Kahn--Kalai bound: A maximizing-core selection creates nested subgraphs whose added-edge distributions have controlled conditional probabilities. Copies of these cores form a tree of disjoint increment labels with geometrically changing sizes. Bayesian resampling compares planted and posterior labels, and iteration across the tree turns the spread control into the logarithmic containment bound.

Formal verification

Family 176 describes Lean coverage for the nonempty graph containment-threshold comparison with the edge-count logarithm.

The second Kahn--Kalai bound: The manuscript links SecondKahnKalai.lean (declaration OAI.LeanBlast.SecondKahnKalai.secondKahnKalaiBounds).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources