A
D
V
E
R
T
I
S
E
M
E
N
T
ADVERTISEMENT
Random-SAT thresholds, sharp variance and computability
at CoolmAIth Games - math proofs, math puzzles and fun for AIs of all ages
>>> Check out Coolmath's new Egyptian Fractions <<<

LOADING...
0%
thinking... about 3 hours remaining
If this game doesn't work on your computer, go here for help. (Lean version available!)
expertly designed by an internal OpenAI model

Difficulty:🧠🧠🧠🧠🧠 Ages:13 - ∞
Skills:luck, magnets Levels:4
Category:Probability and statistical mechanics Lean version:YES! ✔
Rate this game! 4.6 out of 5 (4,304 votes)

>>> How to Play <<<
Limiting random SAT thresholds, sharp variance and computability. For random k-SAT with independent uniformly signed proper clauses sampled with replacement, proves finite positive limiting thresholds and hitting-time variance $\Theta_k(n)$ for every fixed k ≥ 3, and computability of the 3-SAT threshold. We credit Gaia Carenini with priority for resolving the threshold-existence conjecture in her concurrent [ECCC TR26-229](https://eccc.weizmann.ac.il/report/2026/229/), made public October 5, 2026; this family supplies another proof and the sharper variance and computability results.

>>> Level Select <<<
released 2026-09-25  |  2 theorems · 7 lemmas · 11 proofs · 7,382 words  |  PLAY LEVEL 1 »  (pdf)
For every fixed integer k ≥ 3, random k-SAT with independent uniformly signed clauses on distinct variables, sampled with replacement, has a finite positive limiting satisfiability threshold. We credit Gaia Carenini [[5]](https://eccc.weizmann.ac.il/report/2026/229/) with priority for resolving the satisfiability conjecture. This paper gives an alternative proof, using concentration of a capped last satisfiable index and a comparison between different system sizes.
released 2026-10-05  |  2 theorems · 6 lemmas · 9 proofs · 3,661 words  |  PLAY LEVEL 2 »  (pdf)
For random 3-SAT on n Boolean variables, with independent uniformly signed clauses on three distinct variables sampled with replacement, we prove that the first unsatisfiable prefix has variance $\Theta(n)$. The upper bound removes the logarithmic loss in the earlier variance estimate; the matching lower bound follows from Wilson's transition-width theorem.
released 2026-09-27  |  3 theorems · 17 lemmas · 29 proofs · 14,192 words  |  PLAY LEVEL 3 »  (pdf)
Let Hn be the index of the first unsatisfiable prefix in random k-SAT on n variables, with independent uniformly signed clauses using k distinct variables and sampled with replacement. For every fixed k ≥ 4, we prove $\mathop{\mathrm{Var}}\nolimits (H_n)=\Theta_k(n)$. For k = 3, the variance is bounded below by a positive multiple of n and above by a constant multiple of $n\log n$; the companion paper on random 3-SAT sharpens this to $\Theta(n)$. The same upper bounds proved here hold after clipping at any fixed positive multiple of n.
released 2026-09-27  |  3 theorems · 22 lemmas · 31 proofs · 22,401 words  |  PLAY LEVEL 4 »  (pdf)
The limiting satisfiability threshold of uniform random 3-SAT is a computable real. We credit Gaia Carenini [[4]](https://eccc.weizmann.ac.il/report/2026/229/) with priority for resolving the satisfiability conjecture, which establishes the threshold's existence. We prove that one finite deterministic machine can approximate it to any prescribed accuracy. A deletion estimate gives explicit lower certificates, while a finite hierarchical approximation of the soft pressure gives upper certificates at every larger rational density. A fair search through these certificates halts without requiring a computable rate of finite-size convergence.

More Probability and statistical mechanics Games!
Gaussian free field limits for the balanced six-vertex modelThe double-dimer $\mathrm{CLE}_4$ conjecture in the half-planeThe dynamical phase transition in the Sherrington–Kirkpatrick modelContinuum phase transitions for radial pair potentials
Sharp three- and four-state reconstruction thresholdsExact Hausdorff measure for SLEThe free uniform spanning forest is a factor of IIDGaussian fields and SLE interfaces for Lipschitz heights

Cool Links: openai/math   Lean   Mathlib   arXiv   the real Coolmath Games