The threshold for random $k$-SAT is $2^k\log 2-O(k)$

Let $F_k(n,m)$ be a random $k$-CNF formula formed by selecting uniformly and independently $m$ out of all possible $k$-clauses on $n$ variables. It is well known that if $r \geq 2^k \log 2$, then $F_k(n,rn)$ is unsatisfiable with probability that tends to 1 as $n \to \infty$. We prove that if $r \leq 2^k \log 2 - t_k$, where $t_k = O(k)$, then $F_k(n,rn)$ is satisfiable with probability that tends to 1 as $n \to \infty$.

Our technique, in fact, yields an explicit lower bound for the random $k$-SAT threshold for every $k$. For $k \geq 4$ our bounds improve all previously known such bounds.