Random 
-SAT
is a random satisfiability problem in which
a formula on 
Boolean variables is a conjunction of 
independently sampled clauses. Each clause is a disjunction
of 
distinct uniformly chosen variables,
each independently negated with probability 
. The ratio 
is the clause density. Clauses may be repeated.
Vorobyev (2026) reported that for 
and 
, the formula is unsatisfiable
with probability tending to 1 as 
.
Thus 4.268 is an upper bound on the random 3-SAT satisfiability threshold, not its
exact value. Here 
is the floor function. Vorobyev (2026) states that
large language models drove the mathematical argument, Lean formalization, and numerical
code under the author's direction.
