THEOREM 1 — one round of Algorithm A (B) eliminates at least ⅛·|E′| − 1/16 (⅛·|E′|) edges in expectation

Proved

LubyMIS.MonteCarlo.theorem1

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

maximal-independent-setp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1parallel-algorithmsrandomized-algorithms

Let $G' = (V', E')$ be the current graph before the $k$ -th execution of the body of the while loop of Luby's MIS algorithm, and let $n \ge 1$ be the number of vertices of the input graph, so $|V'| \le n$ . Write $Y_k = |E'|$ and $Y_{k+1}$ for the number of edges after that execution, i.e. after removing $I' \cup N(I')$ where $I'$ is produced by the select step.

For Algorithm A (independent uniform priorities in $\{1, \dots, n^4\}$ ; $I'$ the strict local minima),

E\big[Y_k^A - Y_{k+1}^A\big] \;\ge\; \frac18\, Y_k^A - \frac1{16}.

For Algorithm B (independent coins with $\Pr[\mathrm{coin}(i) = 1] = 1/(2d(i))$ , and $1$ if $d(i) = 0$ ; $I'$ the marked vertices whose marked neighbours all have smaller degree),

E\big[Y_k^B - Y_{k+1}^B\big] \;\ge\; \frac18\, Y_k^B.

Each round thus removes a constant fraction of the remaining edges in expectation, which is what makes the expected number of rounds of both algorithms $O(\log n)$ .

Formalization Note The expectation is taken for a fixed current graph $G'$ , i.e. conditionally on the history of the first $k - 1$ rounds, as in the paper's proof ("Let $G' = (V', E')$ be the graph before the $k$ th execution"); the unconditional statement follows by averaging. $n$ is a parameter with $1 \le n$ and $|V'| \le n$ , not $|V'|$ itself. Expectations are finite sums over the $(n^4)^{|V'|}$ priority vectors and the $2^{|V'|}$ coin vectors.

Preamble

import Mathlib
import Definitions.Def_LubyMIS_MonteCarlo_Basic

Formal statement

namespace LubyMIS.MonteCarlo

/-- THEOREM 1 (Luby 1986, §3.4, p. 1040). For the current graph `H = G′` and `n ≥ max(1, |V′|)` the
number of vertices of the input graph, one execution of the loop body eliminates in expectation
(1) at least `⅛ · |E′| − 1/16` edges under Algorithm A, and
(2) at least `⅛ · |E′|` edges under Algorithm B. -/
theorem theorem1 {V : Type*} [Fintype V] [DecidableEq V] (n : ℕ) (hn : 1 ≤ n)
    (hV : Fintype.card V ≤ n) (H : SimpleGraph V) [DecidableRel H.Adj] :
    expA n (fun π => (eliminated H (selectA H π) : ℝ)) ≥
        1 / 8 * (H.edgeFinset.card : ℝ) - 1 / 16 ∧
      expB H (fun c => (eliminated H (selectB H c) : ℝ)) ≥ 1 / 8 * (H.edgeFinset.card : ℝ) := by sorry

end LubyMIS.MonteCarlo

Source

Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4), 1986, p. 1040, §3.4, THEOREM 1 (1) and (2)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Throughout, $V$ is an arbitrary finite type of vertices with decidable equality. $n$ is a natural number and $H$ is a simple graph on $V$ with a decidable adjacency relation. The statement uses five objects from the imported module Definitions.Def_LubyMIS_MonteCarlo_Basic: expA, expB, selectA, selectB and eliminated. Their definitions are not part of the code under audit. This read-back therefore cannot unfold them, and it describes them only by how the statement uses them:

$\mathrm{expA}_n(f)$ is a real number built from $n$ and a real-valued function $f$ of some argument $\pi$ , whose type is fixed by that module (it may depend on $n$ ).
$\mathrm{expB}_H(g)$ is a real number built from the graph $H$ and a real-valued function $g$ of some argument $c$ , whose type is also fixed by that module (it may depend on $H$ ).
$\mathrm{selectA}(H,\pi)$ and $\mathrm{selectB}(H,c)$ are objects built from $H$ and $\pi$ , or from $H$ and $c$ .
$\mathrm{eliminated}(H,S)$ is a quantity built from $H$ and such an object $S$ , then converted into a real number. It is most likely a natural-number count, but that is not visible here.

The statement's names and its doc comment suggest that these are expectations, random selection rules and an eliminated-edge count. The code shown does not establish any of that.

Hypotheses. Both of the following hold:

$1 \le n$ ;
$|V| \le n$ , where $|V|$ is the number of vertices.

Conclusion. Let $|E(H)|$ be the number of edges of $H$ . Both inequalities hold together:

\mathrm{expA}_n\Big(\pi \mapsto \mathrm{eliminated}\big(H, \mathrm{selectA}(H,\pi)\big)\Big) \;\ge\; \tfrac{1}{8}\,|E(H)| - \tfrac{1}{16},

\mathrm{expB}_H\Big(c \mapsto \mathrm{eliminated}\big(H, \mathrm{selectB}(H,c)\big)\Big) \;\ge\; \tfrac{1}{8}\,|E(H)|.

Both bounds are non-strict ( $\ge$ ) and are compared as real numbers. The number $n$ appears only in the first inequality, as the parameter of $\mathrm{expA}$ . The second inequality does not mention $n$ at all, so the hypotheses on $n$ restrict it only through the requirement that some $n$ satisfying them exists; one always does, namely $n=\max(1,|V|)$ . The integer $n$ must be at least $\max(1,|V|)$ but may be arbitrarily larger than $|V|$ , and the first inequality is claimed for every such $n$ .

Degenerate cases. The hypotheses allow $V$ to be empty, since $|V| = 0 \le n$ holds for every $n \ge 1$ . They also allow $V$ to have one vertex, or $H$ to have no edges at all. In every such case $|E(H)| = 0$ , and the statement reduces to:

$\mathrm{expA}_n(\cdots) \ge -\tfrac{1}{16}$ ;
$\mathrm{expB}_H(\cdots) \ge 0$ .

The hypotheses $1 \le n$ and $|V| \le n$ can always be satisfied, so the statement is not vacuous. Whether these degenerate cases hold trivially depends on the imported definitions, which are not shown. For example, it depends on what $\mathrm{expA}$ and $\mathrm{expB}$ return when their domain is empty, or when a normalisation involves dividing by zero, which Lean evaluates to $0$ . It also depends on whether $\mathrm{eliminated}$ can be negative. None of this can be determined from the code given. The statement contains no subtraction in $\mathbb{N}$ : the $-\tfrac{1}{16}$ is taken in $\mathbb{R}$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph