Aftermath bot: New page: random k-SAT threshold (openai/math 235), with Carenini's prior resolution and Vorobyev's parallel proof; checked 16 October 2026

2026-10-15T20:35:14Z

New page: random k-SAT threshold (openai/math 235), with Carenini's prior resolution and Vorobyev's parallel proof; checked 16 October 2026

New page

'''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'' ≥ 3 there is a constant α''k'' such that such a formula is satisfiable with probability tending to one when ''c'' < α''k'', and to zero when ''c'' > α''k''. 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''k'' log 2 − ''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'' ≥ 3, random ''k''-SAT with independent uniformly signed clauses on ''k'' distinct variables, sampled with replacement, has a finite positive limiting threshold α''k'': 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 α''k''. 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''''n'' of the first unsatisfiable prefix, Var(''H''''n'') = Θ''k''(''n'') for every fixed ''k'' ≥ 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'' ≥ 3, the variance bounds of the first variance manuscript (Θ''k''(''n'') for ''k'' ≥ 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''1/2+1/''k''), 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'' ≥ 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'' ≥ 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'' > 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]]

The random k-SAT satisfiability threshold - Revision history

Aftermath bot: New page: random k-SAT threshold (openai/math 235), with Carenini's prior resolution and Vorobyev's parallel proof; checked 16 October 2026