# The second Kahn–Kalai conjecture with an edge-count bound

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

- [The second Kahn–Kalai conjecture](../../preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf)

## Scope

The second Kahn–Kalai conjecture compares the threshold for a random graph to contain a fixed graph with its expectation threshold. The formalized result proves the comparison up to a universal factor times $1+\log_2|E(H)|$, and hence up to a universal factor times $\log_2 n$, for every graph $H$ with at least one edge and at most $n$ vertices, $n\ge2$. The bounds use the actual containment and expectation thresholds.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Second Kahn–Kalai threshold bounds | [SecondKahnKalai.lean](../ComparatorChallenges/SecondKahnKalai.lean) |