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, numerical
code, and manuscript preparation under the author's direction.
