# Correspondence coloring with a fixed forbidden subgraph

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A logarithmic independence bound for clique-free graphs](../../preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026/paper.pdf)

## Scope

The formalized result gives a logarithmic improvement in the independence number of clique-free graphs. For every fixed integer $r\ge4$, there is $c_r>0$ such that every finite $K_r$-free simple graph on $n$ vertices with average degree $d\ge2$ has an independent set of size at least $c_r n\log d/d$. The constant depends only on $r$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Logarithmic independence bound for clique-free graphs | [CliqueFreeLog.lean](../ComparatorChallenges/CliqueFreeLog.lean) |