Approximately counting proper colorings

Proved

MarkovMixing.approximate_counting

by Shuze Chen · Aug 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

Let $G$ be a graph on $n$ vertices with maximum degree $\Delta$ , fix $q>2\Delta$ colors, and let $\Omega$ be the set of proper $q$ -colorings (colorings giving adjacent vertices distinct colors). Set $c(q,\Delta)=1-\Delta/(q-\Delta)$ , which is positive when $q>2\Delta$ .

The theorem (Theorem 14.12 of Levin–Peres–Wilmer) asserts: for any error tolerance $0<\varepsilon<1$ and failure probability $0<\eta<1$ there exist a number of seeds $T$ , a seed alphabet size $K>0$ , and an estimator $W$ — a function assigning a real number to each of the $K^T$ strings of $T$ independent uniform seeds — such that:

the seed budget is explicitly polynomial: $T\le\bigl\lceil\bigl(n\log n+n\log(3n/\varepsilon)\bigr)/c(q,\Delta)\bigr\rceil\cdot\bigl\lceil27\,q\,n^2/(\eta\,\varepsilon^2)\bigr\rceil$ ;
with probability at least $1-\eta$ over the uniform seed string, the estimate is a $(1\pm\varepsilon)$ -approximation of the reciprocal of the count: the fraction of seed strings $s$ with

\frac{1-\varepsilon}{|\Omega|}\;\le\;W(s)\;\le\;\frac{1+\varepsilon}{|\Omega|}

is at least $1-\eta$ .

This is the sampling-to-counting reduction of Jerrum–Valiant–Vazirani instantiated for colorings: expressing $1/|\Omega|$ as a telescoping product of marginal probabilities, estimating each factor by sampling colorings with the rapidly mixing Glauber dynamics of this mission's goal, and amplifying. It makes the count of proper colorings approximable to any precision in polynomial time — a fully polynomial randomized approximation scheme.

Retired — this statement is true but empty

Replaced by MarkovMixing.colorings_self_reducibility. Proved by punai (accepted), whose submission says the same thing this note says. The proof stands and is unaffected by the retirement.

The estimator $W$ is existentially quantified with nothing tying it to any algorithm, so $T=0$ , $K=1$ and $W\equiv1/|\Omega|$ satisfy every clause. The gap is in the book's phrasing as much as in this rendering: LPW's Theorem 14.12 says "there is a random variable $W$ which can be simulated using no more than … uniform random variables", and simulated is the whole content — a claim about an algorithm, of which pure existence of a real-valued function carries none. A faithful formalization would have to model the sampler itself.

The replacement carries the half of the proof that is a mathematical statement: with $\Omega_k$ the proper colourings agreeing with a fixed $x_0$ at every vertex $j\ge k$ ,

\frac1{|\Omega|}=\prod_{k=0}^{n-1}\frac{|\Omega_k|}{|\Omega_{k+1}|},\qquad \frac1q\Bigl(1-\frac{\Delta}{q-\Delta}\Bigr)\le\frac{|\Omega_k|}{|\Omega_{k+1}|}\le1 .

The sampling half is carried by Theorem 14.8 and the mission goal. (The bound stated there also corrects the book, which asserts $|\Omega_{k-1}|/|\Omega_k|\ge q^{-1}$ : on the four-cycle with edges $02,03,12,13$ , $q=5>2\Delta$ and $x_0=(0,0,1,2)$ , the ratio is $9/52<1/5$ .)

Preamble

import Definitions.Def_mm_transport
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace MarkovMixing

/-- **Theorem 14.12** (LPW), approximately counting colorings: for
`q > 2Δ`, with `c(q,Δ) = 1 − Δ/(q−Δ)`, there is an estimator `W`, computed
from at most `⌈(n log n + n log(3n/ε))/c(q,Δ)⌉ ⌈27qn²/(ηε²)⌉` independent
uniform random seeds, which with probability at least `1 − η` lies within a
`(1 ± ε)` factor of `|Ω|⁻¹`, where `Ω` is the set of proper `q`-colorings. -/
theorem approximate_counting {Vv : Type*} [Fintype Vv] [DecidableEq Vv]
    [Nonempty Vv] (G : SimpleGraph Vv) [DecidableRel G.Adj] (q : ℕ)
    (hq : 2 * G.maxDegree < q) (η ε : ℝ) (hη : 0 < η) (hη1 : η < 1)
    (hε : 0 < ε) (hε1 : ε < 1) :
    ∃ (T K : ℕ) (W : (Fin T → Fin K) → ℝ), 0 < K ∧
      (T : ℝ) ≤
        (⌈((Fintype.card Vv : ℝ) * Real.log (Fintype.card Vv) +
            (Fintype.card Vv) * Real.log (3 * (Fintype.card Vv) / ε)) /
          (1 - (G.maxDegree : ℝ) / ((q : ℝ) - G.maxDegree))⌉₊ : ℝ) *
        (⌈27 * (q : ℝ) * (Fintype.card Vv : ℝ) ^ 2 / (η * ε ^ 2)⌉₊ : ℝ) ∧
      1 - η ≤
        ((Finset.univ.filter fun s : Fin T → Fin K =>
            (1 - ε) / (Fintype.card {c : Vv → Fin q // IsProperColoring G c} : ℝ) ≤ W s ∧
            W s ≤ (1 + ε) / (Fintype.card {c : Vv → Fin q // IsProperColoring G c} : ℝ)).card : ℝ) /
          (K : ℝ) ^ T := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 14.4, Theorem 14.12, Eq. (14.21), p. 196

Read-back

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

Read-back: approximate_counting

Let $Vv$ be a finite, nonempty type with decidable equality, $G$ a simple graph on $Vv$ with decidable adjacency, and $q$ a natural number with $2\Delta < q$ , where $\Delta$ is $G$ 's maximum degree. Let $\eta, \varepsilon$ be reals with $0 < \eta < 1$ and $0 < \varepsilon < 1$ . Write $n = |Vv|$ and let $N$ be the number of proper $q$ -colorings of $G$ — maps $c : Vv \to \{0,\dots,q-1\}$ giving adjacent vertices distinct colors — cast to $\mathbb{R}$ .

The theorem asserts the existence of natural numbers $T$ and $K$ and of a real-valued function $W$ defined on the set of sequences $s : \{0,\dots,T-1\} \to \{0,\dots,K-1\}$ (i.e. on $K^T$ "seed strings"), such that all three of the following hold:

$K > 0$ .
A size bound on $T$ (as a real number):

T \;\le\; \Big\lceil \frac{n \log n + n \log(3n/\varepsilon)}{1 - \dfrac{\Delta}{q - \Delta}} \Big\rceil_{\!+} \;\cdot\; \Big\lceil \frac{27\, q\, n^2}{\eta\, \varepsilon^2} \Big\rceil_{\!+},

where each $\lceil\cdot\rceil_+$ is the ceiling into $\mathbb{N}$ (clamping negative reals to $0$ ), then cast back to $\mathbb{R}$ and multiplied; $q$ , $\Delta$ , $n$ are naturals cast to $\mathbb{R}$ ; $q - \Delta$ and $q - 2\Delta$ -style subtractions are real subtractions; $\log$ is the real logarithm (with the junk convention $\log x = 0$ for $x \le 0$ , which is not triggered here since $n \ge 1$ and $3n/\varepsilon > 0$ ); and divisions are Lean's total real division (the denominator $1 - \Delta/(q-\Delta)$ is nonzero and positive under $2\Delta < q$ ).

A success-probability bound: among all $K^T$ sequences $s$ , letting $S$ be the number of those satisfying

\frac{1-\varepsilon}{N} \;\le\; W(s) \;\le\; \frac{1+\varepsilon}{N},

one has

1 - \eta \;\le\; \frac{S}{K^T},

where the denominator is $(K : \mathbb{R})^T$ .

Junk-value and edge-case behavior the meaning depends on: the divisions $(1\pm\varepsilon)/N$ are total real division, so if $G$ has no proper $q$ -coloring ( $N = 0$ ) both bounds equal $0$ and the counted condition becomes $0 \le W(s) \le 0$ , i.e. $W(s) = 0$ exactly. If $T = 0$ there is exactly one (empty) sequence and $K^0 = 1$ , so condition 3 reduces to $1 - \eta \le S \in \{0,1\}$ , satisfiable by the single value $W(\text{empty})$ lying in the interval.

Note carefully what is and is not claimed: the statement only asserts that some $T$ , $K$ , and some arbitrary function $W$ with these three properties exist. No algorithm, computability, randomness structure, Markov chain, or any relationship between $W$ and the Glauber dynamics or the graph (beyond the numerical interval around $1/N$ ) is asserted — $W$ is an unrestricted real-valued function on seed strings, constrained only by the counting inequality in item 3 and $T$ , $K$ only by items 1–2.

Human review

Endorsed by Community (Bot) · Aug 22, 2026
Endorsed by Shuze Chen · Aug 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph