The satisfiability threshold conjecture: a limiting random k-SAT threshold for every k >= 3

Fix $k\ge3$ and let $F_{n,m}$ be a conjunction of $m$ independent uniformly random $k$ -clauses on $n$ Boolean variables (distinct variables in a clause, fair signs). Friedgut (with Bourgain) proved a sharp threshold: there is a sequence $c_k(n)$ around which the satisfiability probability drops from near one to near zero, but not that $c_k(n)$ converges. Ding, Sly and Sun proved convergence, with the predicted value, for all sufficiently large $k$ ; the case $k=2$ is classical. Chvatal and Reed conjectured that each fixed clause size has a limiting density. Is there, for every fixed $k\ge3$ , a constant $\alpha_k$ such that $\Pr(F_{n,\lfloor cn\rfloor}\text{ satisfiable})\to1$ for $c<\alpha_k$ and $\to0$ for $c>\alpha_k$ ?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Random constraint satisfaction; random k-SAT phase transition
Posed by: Vasek Chvatal and Bruce Reed (Mick gets some (the odds are on his side), FOCS 1992)
Year posed: 1992
Years open: 34y
Solved: 2026-09-25
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 42 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Claims Theorem 1.1: for every fixed $k\ge3$ there is $\alpha_k\in(0,\infty)$ with $\Pr(F_{n,\lfloor cn\rfloor}\in\mathrm{SAT})\to1$ for $c<\alpha_k$ and $\to0$ for $c>\alpha_k$ ; it says nothing at $c=\alpha_k$ and does not identify $\alpha_k$ for small $k$ . Companions claim hitting-time variance $\Theta_k(n)$ for $k\ge4$ and $\Theta(n)$ for $k=3$ , and that $\alpha_3$ is a computable real. Priority: the release credits Gaia Carenini's ECCC TR26-229 (made public 5 October 2026) with first resolving the existence conjecture; this is an independent second proof of the same result, not a contradiction.

What the AI did

Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems. The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is authored as OpenAI with no human author named. The release itself credits Gaia Carenini (ECCC TR26-229, public 5 October 2026) with priority for the threshold-existence result and presents this family as an alternative proof plus sharper variance and computability results.

Verification

No independent mathematician has checked this yet. Checked here: abstract, introduction and Theorem 1.1 of the principal manuscript, and the abstracts of the three companions, read against Chvatal and Reed's conjecture as cited. The proofs were not refereed. Scope stated by the paper: clauses on distinct variables sampled with replacement; strict-side statement, nothing at $c=\alpha_k$ ; the value of $\alpha_k$ is not identified. Lean-checked on the release's own Comparator challenge FixedClauseThreshold together with its solution module OAI.Probability.RandomSAT.Main, both fetched at the pinned commit; the challenge is not listed in the release's formalization catalogue (lean/formalization.yaml), the statement was read here but not independently audited, and the development was not rebuilt here. The formal statement (OAI.FixedClauseThreshold.main) says: for every k >= 3 there is a real alpha > 0 such that the satisfiability probability (literal finite counting ratio) at floor(c n) clauses tends to 1 for 0 <= c < alpha and to 0 for c > alpha. That is the headline claim. The variance (SATVariance) and 3-SAT computability (SATComputability) challenges also exist with solution modules; they were not read in detail.

The satisfiability threshold conjecture: a limiting random k-SAT threshold for every k >= 3

What was actually shown

What the AI did

Verification

Sources

Discussion