we-solve (beta)

Math-2609-A1 · revision r1 · on Math-2609

OpenAI claim summary for Math-2609

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: 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 graph-property theorem gives the requested quantile-width estimate with universal constant $2^{19}$, for every $n\ge2$, every nontrivial increasing property invariant under vertex permutations, and each $0<\varepsilon<1/2$. Its parameter $n$ counts vertices, as in this question.

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

Manuscript

Contents
  1. Log-squared sharp threshold for monotone graph properties
  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

Log-squared sharp threshold for monotone graph properties

OpenAI's claim

Sharp thresholds for graph properties: The claimed threshold interval for a vertex-invariant increasing graph property has width at most a universal multiple of $\log(1/(2\varepsilon))/(\log n)^2$. This comparison uses the probabilities $\varepsilon$ and $1-\varepsilon$.

Mathematical statement of the claimed result

Mathematical claim 1.
Let $\mathcal P$ be a nontrivial increasing property of simple graphs on $n\ge2$ vertices, unchanged when vertex labels are permuted. Write $p_a=\inf\{p:\mathbb P(G(n,p)\in\mathcal P)\ge a\}$. For every $0<\epsilon<1/2$ the claimed sharp-threshold bound is \[p_{1-\epsilon}-p_\epsilon\le\frac{2^{19}}{(\log n)^2}\log\frac1{2\epsilon}.\] Logs are natural and $n$ counts vertices rather than potential edges.

Outline of the argument

Sharp thresholds for graph properties: A random block of vertices is retained while all edges disjoint from it are conditioned upon, preserving a useful permutation symmetry. A biased Fourier estimate bounds conditional low-degree mass linearly in influence. A small-degree vertex in each indexing graph transfers that bound to a larger original degree range, and integration of the probability derivative gives the quantile width.

Formal verification

Family 186 describes Lean coverage for the graph-property threshold width; the hypergraph refinement is not part of this selection.

Sharp thresholds for graph properties: The manuscript links SharpThreshold.lean.

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