Version history

Submission versions

  1. lax-965890current version

    Constructive Lovász Local Lemma

  2. lax-296731

    Constructive Lovász Local Lemma

  3. lax-41viewing

    Constructive Lovász Local Lemma

    GitHub sourceShown on this page

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Proof of `The Moser–Tardos theorem`

groundedproofs/Lax41Proofs/MoserTardos.lean · lax-41

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The Moser–Tardos witness-tree argument. An infinite table supplies every fresh sample used by the algorithm. Each resampling occurrence injects into a proper witness tree, the probability that a fixed tree occurs is the product of its event probabilities, and the branching-process estimate sums these products. Finiteness of that sum also yields a terminating table and hence an assignment avoiding all bad events.