Linear variance of the random 3-SAT unsatisfiability time
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
Let $H_n$ be the first clause count at which sequential independent uniformly signed proper 3-clauses make an n-variable formula unsatisfiable. Are there absolute $c,C>0$ such that $cn\leq Var(H_n)\leq Cn$ for all sufficiently large n?Short English statement
Let $H_n$ be the first clause count at which sequential independent uniformly signed proper 3-clauses make an n-variable formula unsatisfiable. Are there absolute $c,C>0$ such that $cn\leq Var(H_n)\leq Cn$ for all sufficiently large n?Sources
- S1 Original question source or mathematical context. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026/build/source/main.tex.
- S2 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2904
For proper random 3-SAT clauses sampled with replacement, the uncapped first-unsatisfiable hitting time is claimed to have variance $\Theta(n)$. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.
Linear variance of the random 3-SAT unsatisfiability time
OpenAI's claim
OpenAI presents a proof in the selected manuscript. For proper random 3-SAT clauses sampled with replacement, the uncapped first-unsatisfiable hitting time is claimed to have variance $\Theta(n)$.Mathematical statement of the claimed result
Result 1.
Sample independent clauses, with replacement, uniformly among the $2^k\binom nk$ signed clauses on $k$ distinct variables. Write $F_m=\bigwedge_{j=1}^mC_j$ and $H_n=\min\{m\ge1:F_m\text{ is unsatisfiable}\}$. For $k=3$, an absolute $C<\infty$ gives \[ \operatorname{Var}(H_n)\le Cn\quad(n\ge3). \] There are also absolute $c>0,n_0$ with $\operatorname{Var}(H_n)\ge cn$ for $n\ge n_0$. Thus $\operatorname{Var}(H_n)=\Theta(n)$.Outline of the argument
A new potential sums the probabilities that successive two-clauses kill a given assignment set. This improves the critical occupation estimate in the deletion-delay framework, removes the logarithmic upper-bound loss, and combines cap removal with the established transition-width lower bound.Formal verification
For family 235, the selected entries establish threshold existence, threshold computability, linear variance for $k\geq4$, and the earlier $O(n\log n)$ bound for $k=3$. The later linear three-clause variance improvement is not selected. No Comparator is assigned to the selected manuscript here; the family page selects other papers or supporting statements. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.Status caveat
OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.Sources
- OpenAI, Linear Variance of the Random 3-SAT Hitting Time, 2026-10-05; citation key
OAI:Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 235: Lean scope.
- OpenAI catalogue entry.