View source for The random k-SAT satisfiability threshold

'''The random k-SAT satisfiability threshold''' concerns random formulas with ''n'' Boolean variables and about ''cn'' independent random clauses of ''k'' literals. The satisfiability conjecture asserts that for each fixed ''k'' &ge; 3 there is a constant α<sub>''k''</sub> such that such a formula is satisfiable with probability tending to one when ''c'' &lt; α<sub>''k''</sub>, and to zero when ''c'' &gt; α<sub>''k''</sub>. Manuscripts dated from 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) give a proof of this existence statement together with variance and computability results. The collection credits Gaia Carenini, whose report made public on 5 October 2026 resolves the conjecture, with priority. A further proof with a Lean formalization was posted on GitHub on 6 October 2026. This page summarizes the published claims and lists related public work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the first manuscript: Chvátal and Reed formulated the conjecture that each fixed clause size has a limiting satisfiability density, and settled the two-clause case (with independent proofs credited to Goerdt and to Fernandez de la Vega). Friedgut's sharp-threshold theorem, with an appendix by Bourgain, showed that random ''k''-SAT has a sharp transition around a sequence of densities, leaving open whether that sequence converges. Achlioptas and Peres obtained the bounds 2<sup>''k''</sup> log 2 &minus; ''O''(''k''); the cavity method of statistical physics (Mézard, Parisi and Zecchina; Mertens, Mézard and Zecchina) predicted the threshold; Coja-Oghlan and Panagiotou located it up to an error tending to zero as ''k'' grows; and Ding, Sly and Sun proved existence, with the value predicted by one-step replica symmetry breaking, for all sufficiently large ''k''.

== The original results ==
* '''Threshold existence.''' For every fixed ''k'' &ge; 3, random ''k''-SAT with independent uniformly signed clauses on ''k'' distinct variables, sampled with replacement, has a finite positive limiting threshold α<sub>''k''</sub>: below it the satisfiability probability tends to one, above it to zero. The statement says nothing at the threshold itself and does not identify the value of α<sub>''k''</sub>. The manuscript credits Carenini with priority for the resolution of the conjecture and presents its argument as an alternative proof.
* '''Variance of the hitting time.''' For the index ''H''<sub>''n''</sub> of the first unsatisfiable prefix, Var(''H''<sub>''n''</sub>) = Θ<sub>''k''</sub>(''n'') for every fixed ''k'' &ge; 4; for ''k'' = 3 the first variance manuscript gives a linear lower bound and an ''O''(''n'' log ''n'') upper bound, and a later manuscript sharpens this to Θ(''n'').
* '''Computability.''' The limiting threshold of uniform random 3-SAT is a computable real: one deterministic machine approximates it to any prescribed accuracy, without assuming a computable rate of finite-size convergence.
* '''Sources''' (openai/math repository, commit <code>1581d4c</code>):
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026 ''A Limiting Satisfiability Threshold for Every Fixed Clause Size''] (25 September 2026);
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026 ''Variance of the Random k-SAT Hitting Time''] (27 September 2026);
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026 ''Computing the Random 3-SAT Threshold''] (27 September 2026);
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026 ''Linear Variance of the Random 3-SAT Hitting Time''] (5 October 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/235.md lean/docs/235.md] states that the formalization proves the existence of the threshold for every fixed ''k'' &ge; 3, the variance bounds of the first variance manuscript (Θ<sub>''k''</sub>(''n'') for ''k'' &ge; 4; for ''k'' = 3 a linear lower bound and an ''O''(''n'' log ''n'') upper bound), and the computability of the 3-SAT threshold. The manuscript of 5 October 2026 is not among the papers listed in the scope note.

== Related work by others ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-05 || Gaia Carenini, [https://eccc.weizmann.ac.il/report/2026/229/ ECCC TR26-229], ''A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture'' || Earlier resolution (credited with priority by the collection) || The scaling window of random ''k''-SAT has width ''O''(''n''<sup>1/2+1/''k''</sup>), a polynomial improvement over the author's earlier bound ''O''(''n''/log ''n'') (ECCC TR26-145, [https://arxiv.org/abs/2609.26222 arXiv:2609.26222]); combined with a result of Abbe and Montanari, this establishes the satisfiability conjecture for every fixed ''k'' &ge; 3. || ECCC report, published 5 October 2026. The collection's entry and manuscripts credit Carenini with priority for resolving the conjecture.
|-
| 2026-10-06 || Fedor Vorobyev, [https://github.com/yamelton/sat-constant-threshold yamelton/sat-constant-threshold] (GitHub) || Parallel proof (formalization) || A direct argument for a constant sharp satisfiability threshold for every fixed ''k'' &ge; 3 in the same model (uniform signs, ''k'' distinct variables, repeated clauses allowed), with a 12-page paper and a Lean 4 formalization whose final theorem is <code>SatThreshold.Width.SimpleThreshold.constant_sharp_threshold</code>. It does not compute the value of the threshold. || GitHub repository, first commit 6 October 2026, described as a preprint for review. The README states that the formal proof was checked locally with Lean 4.24.0 and depends only on the three standard axioms, that Carenini's TR26-229 already states the same existence theorem with stronger bounds for ''k'' &gt; 3, that no priority is claimed, and that large language models contributed substantially.
|}

== Notes ==
* Dates are those shown by ECCC, GitHub and the manuscripts. The list covers sources found up to the date above; it makes no priority or completeness claim beyond the credits stated by the sources themselves.

[[Category:OpenAI results]]