An upper bound of 4.268 for the random 3-SAT satisfiability threshold

Fedor Vorobyev

cs.DM Oct 6, 2026 · v1 math.PR

formalization mathlib probability combinatorics

Read PDF arXiv abstract Code

TL;DR

The full proof of the 4.268 upper bound for the random 3-SAT threshold, including the exact rational certificate computation, is formalized in Lean 4 with Mathlib.

Abstract

We prove that a random 3-SAT formula with $n$ variables and $\lfloor 4.268n\rfloor$ clauses is unsatisfiable with high probability. The satisfiability threshold has attracted considerable attention: successive upper bounds reached 4.4898 in the work of Díaz, Kirousis, Mitsche, and Pérez-Giménez, while the cavity method predicts a value near 4.267. Our bound brings the rigorous upper estimate close to this prediction. The proof builds on earlier interpolation methods, including the energetic approach of Achlioptas and Menchaca-Méndez. We study the smallest number of clauses that any assignment must violate, comparing the random formula with a simpler system of constraints on individual variables. This comparison reduces the bound to a finite calculation, which we verify using exact rational arithmetic. The proof is formalized in Lean 4.

Problem

The random 3-SAT satisfiability threshold is predicted by the cavity method to be near 4.267. The best previous rigorous upper bound was 4.4898. The goal is to prove that random 3-SAT formulas with ⌊4.268n⌋ clauses are unsatisfiable with high probability.

Approach

An interpolation argument compares the minimum number of violated clauses in the random formula with a simpler system of single-variable site constraints. The comparison uses a local cubic inequality (B−C)^2(B+2C)≥0 and Poisson clause/site counts. The site-only bound reduces to a finite calculation, certified with exact rational arithmetic and interval enclosures of exponentials computed inside Lean. Concentration via a Doob martingale variance bound and Chebyshev's inequality yields unsatisfiability with high probability.

Results

Random 3-SAT with ⌊4.268n⌋ clauses is unsatisfiable with high probability, close to the cavity prediction of about 4.267. The rational certificate inequality V+W ≤ −1/100000 and the whole argument are machine-checked in Lean 4 with Mathlib. Sources are available on GitHub.

Contribution	Independent upper bound
Site contribution	-0.7611927541550103
Clause-replacement correction	+0.7611815516097719
Sum	-0.000011202545238429759

Independent upper bounds on the certificate contributions (rounded, cross-check only)

Papers With

An upper bound of 4.268 for the random 3-SAT satisfiability threshold