Random independent sets and local sparsity
Ewan Davies
math.CO
Sep 4, 2026 · v1
TL;DR
The main results were formalized in Lean 4 with Mathlib, with the Lean proofs generated almost entirely by AI; release is planned.
Abstract
We analyze random constructions of independent sets in locally sparse graphs, specifically graphs with bounded maximum average degree in neighborhoods or with fractionally $r$-colorable neighborhoods. Specializing our methods to finding large independent sets and low-weight fractional colorings, we focus on optimizing for marginals, but we also derive results that find many independent sets (i.e.\ give lower bounds on the independence polynomial) by optimizing for entropy. Our main results generalize the local Shearer bound of Martinsson and Steiner for triangle-free graphs to graphs with few triangles and to graphs with fractionally $r$-colorable neighborhoods, in the latter case improving upon a result of Dhawan. We also extend independence polynomial bounds obtained via induction to such graphs, improving upon known bounds obtained by local occupancy by relaxing the necessary hypotheses from a maximum degree condition to an average degree condition.
Problem
The paper seeks lower bounds on vertex marginals of random independent sets, and on the independence polynomial, in locally sparse graphs. These are graphs with few triangles or with fractionally r-colorable neighborhoods, going beyond the triangle-free setting.
Approach
Random constructions of independent sets are analyzed by induction on the vertex count. A random experiment picks an induced subgraph and a partial independent set, and the marginal analysis forces the additive error to vanish. For independence polynomial bounds, a variational entropy identity is combined with random pivot vertex choices. The main results were also formalized in Lean 4 with Mathlib using AI-generated proofs.
Results
The local Shearer bound of Martinsson and Steiner is generalized to graphs with few triangles and to graphs with fractionally r-colorable neighborhoods, improving a result of Dhawan. Independence polynomial bounds are extended under average-degree rather than maximum-degree hypotheses.
