Jump to content

The random k-SAT satisfiability threshold

From OpenAI Aftermath

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 (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 2k 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 Hn of the first unsatisfiable prefix, Var(Hn) = Θ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 1581d4c):
  • Formalization, as described by the repository. The scope note 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.
Date Work Relation Public claim Public status (checked 16 October 2026)
2026-10-05 Gaia Carenini, 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(n1/2+1/k), a polynomial improvement over the author's earlier bound O(n/log n) (ECCC TR26-145, 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, 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 SatThreshold.Width.SimpleThreshold.constant_sharp_threshold. 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.
Retrieved from "https://openai-aftermath.mathnt.net/index.php?title=The_random_k-SAT_satisfiability_threshold&oldid=158"