Probability and statistical mechanics · Result 235

Limiting random SAT thresholds, sharp variance and computability

4 papersLean

For random k-SAT with independent uniformly signed proper clauses sampled with replacement, proves finite positive limiting thresholds and hitting-time variance \(\Theta_k(n)\) for every fixed k ≥ 3, and computability of the 3-SAT threshold. We credit Gaia Carenini with priority for resolving the threshold-existence conjecture in her concurrent ECCC TR26-229, made public October 5, 2026; this family supplies another proof and the sharper variance and computability results.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 4

A Limiting Satisfiability Threshold for Every Fixed Clause Size

OpenAI · September 25, 2026

For every fixed integer k ≥ 3, random k-SAT with independent uniformly signed clauses on distinct variables, sampled with replacement, has a finite positive limiting satisfiability threshold. We credit Gaia Carenini [[5]](https://eccc.weizmann.ac.il/report/2026/229/) with priority for resolving the satisfiability conjecture. This paper gives an alternative proof, using concentration of a capped last satisfiable index and a comparison between different system sizes.

Read PDF Download Source

Cite

@misc{OAI:A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026,
  author = {{OpenAI}},
  title = {{A Limiting Satisfiability Threshold for Every Fixed Clause Size}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf}{OAI:A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026}},
  year = {2026}
}

Linear Variance of the Random 3-SAT Hitting Time

OpenAI · October 5, 2026

For random 3-SAT on n Boolean variables, with independent uniformly signed clauses on three distinct variables sampled with replacement, we prove that the first unsatisfiable prefix has variance \(\Theta(n)\). The upper bound removes the logarithmic loss in the earlier variance estimate; the matching lower bound follows from Wilson's transition-width theorem.

Read PDF Download Source

Cite

@misc{OAI:Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026,
  author = {{OpenAI}},
  title = {{Linear Variance of the Random 3-SAT Hitting Time}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026/linear-variance-of-the-random-3-sat-hitting-time.pdf}{OAI:Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026}},
  year = {2026}
}

Variance of the Random k-SAT Hitting Time

OpenAI · September 27, 2026

Let H_n be the index of the first unsatisfiable prefix in random k-SAT on n variables, with independent uniformly signed clauses using k distinct variables and sampled with replacement. For every fixed k ≥ 4, we prove \(\mathop{\mathrm{Var}}\nolimits (H_n)=\Theta_k(n)\). For k = 3, the variance is bounded below by a positive multiple of n and above by a constant multiple of \(n\log n\); the companion paper on random 3-SAT sharpens this to \(\Theta(n)\). The same upper bounds proved here hold after clipping at any fixed positive multiple of n.

Read PDF Download Source

Cite

@misc{OAI:Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026,
  author = {{OpenAI}},
  title = {{Variance of the Random $k$-SAT Hitting Time}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026/article.pdf}{OAI:Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026}},
  year = {2026}
}

Computing the Random 3-SAT Threshold

OpenAI · September 27, 2026

The limiting satisfiability threshold of uniform random 3-SAT is a computable real. We credit Gaia Carenini [[4]](https://eccc.weizmann.ac.il/report/2026/229/) with priority for resolving the satisfiability conjecture, which establishes the threshold's existence. We prove that one finite deterministic machine can approximate it to any prescribed accuracy. A deletion estimate gives explicit lower certificates, while a finite hierarchical approximation of the soft pressure gives upper certificates at every larger rational density. A fair search through these certificates halts without requiring a computable rate of finite-size convergence.

Read PDF Download Source

Cite

@misc{OAI:Computing-the-Random-3-SAT-Threshold-September-27-2026,
  author = {{OpenAI}},
  title = {{Computing the Random 3-SAT Threshold}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf}{OAI:Computing-the-Random-3-SAT-Threshold-September-27-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The random \(k\)-SAT threshold problem asks whether satisfiability changes at one limiting clause density. The formalization proves that every fixed integer \(k\ge3\) has a finite positive threshold \(\alpha_k\): for every fixed density \(c<\alpha_k\), the satisfiability probability tends to one as the number of variables grows, while for every \(c>\alpha_k\) it tends to zero. Clauses use distinct variables with independent uniform signs and are sampled independently with replacement. The statement makes no assertion at the threshold itself.

Let \(H_n\) be the first unsatisfiable prefix length in random \(k\)-SAT with independent uniformly signed clauses on \(k\) distinct variables, sampled with replacement. The formalization proves \(\mathrm{Var}(H_n)=\Theta_k(n)\) for every fixed \(k\ge4\). For \(k=3\), it proves a positive linear lower bound and an \(O(n\log n)\) upper bound. The same upper bounds hold after clipping at any fixed positive multiple of \(n\), and linear lower bounds hold for sufficiently high clipping levels.

The linked supplements prove sharpness of the separate survival-lifetime and clause-replacement estimates used in the argument. They do not show that the logarithmic factor in the \(k=3\) variance bound is necessary.

The formalization proves that the limiting threshold \(\alpha\) for uniform random \(3\)-SAT is a computable positive real. Satisfiability tends to one at every fixed density below \(\alpha\) and to zero at every fixed density above it. One deterministic machine produces a rational number \(q_r\) for every requested precision \(r\) with \(|q_r-\alpha|\le2^{-r}\). No computable rate of finite-size convergence is assumed in the statement.

Comparator links

Result	Comparator statement
Limiting satisfiability threshold for every fixed \(k\ge3\)	FixedClauseThreshold.lean
Sharpness of random \(k\)-SAT lifetime and replacement bounds	SATSharpness.lean
Variance bounds for the random \(k\)-SAT hitting time	SATVariance.lean
Computability of the random \(3\)-SAT threshold	SATComputability.lean

Scope note on GitHub →