{"id":"palomar/PALOMAR-2026-10-29-000008","url":"https://github.com/jtraverso/moser-tardos/tree/5a3024a6d3eb442ac6925f9b3660b93c36cfb8b4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000008-v1.json","repo":"https://github.com/jtraverso/moser-tardos","tags":["math.CO","math.PR","cs.DS","msc:05D40","msc:60C05","msc:68W20"],"score":0,"title":"The Moser–Tardos theorem (algorithmic Lovász Local Lemma)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Moser–Tardos theorem in the variable setting: finitely many independent random variables with finite ranges, n events each determined by a finite set of variables, neighbours sharing a variable. If P(A_j) ≤ x_j ∏_{k ∈ Γ(j)} (1 − x_k) with 0 ≤ x_j < 1, the resampling algorithm (always resampling the first violated event), run on a random resampling table, resamples A_j at most x_j / (1 − x_j) times in expectation among its first t steps, for every t; the expected total number of resamplings is at most ∑_j x_j / (1 − x_j); the probability that it has not…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"A constructive proof of the general Lovász Local Lemma","identifier":"doi:10.1145/1667053.1667060","relationship":"formalizes"}]}