{"id":"palomar/PALOMAR-2026-10-20-000004","url":"https://github.com/jtraverso/lovasz-local-lemma/tree/9d020fa8fb20e9426c2d6780a3cfab4a68794d89","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000004-v1.json","repo":"https://github.com/jtraverso/lovasz-local-lemma","tags":["math.CO","math.PR","msc:05D40","msc:05C55","msc:05C15","msc:60C05","probabilistic-method","graph-theory","formalization"],"score":0,"title":"The Lovász Local Lemma and two applications","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 Lovász Local Lemma for finitely many events in a probability space with a dependency graph (each event mutually independent, in the sense of Mathlib's `ProbabilityTheory.Indep` of generated σ-algebras, of its non-neighbours), in its general form (P(A_i) ≤ x_i ∏_{j∼i}(1 − x_j) implies P(no event) ≥ ∏(1 − x_i)) and its symmetric form (e p (d + 1) ≤ 1 implies P(no event) > 0); and of two applications: Spencer's Ramsey lower bound (if 2e(C(k,2)C(n,k−2) + 1) ≤ 2^C(k,2) then R(k,k) > n) and the Erdős–Lovász property B theorem for k-uniform hypergraphs (each…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Problems and results on 3-chromatic hypergraphs and some related questions","identifier":"","relationship":"formalizes"},{"title":"Asymptotic lower bounds for Ramsey functions","identifier":"doi:10.1016/0012-365X(77)90044-9","relationship":"formalizes"}]}