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

1 paperLean

Proves the second Kahn–Kalai conjecture: for every finite simple graph H with h ≥ 1 edges and at most n vertices, its appearance threshold in \(G(n,p)\) is at most \(C p_{\mathrm E}(n,H)(1+\log_2 h)\), with universal C. Here \(p_{\mathrm E}\) is the least density at which every subgraph of H has expected copy count at least 1/2.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The second Kahn–Kalai conjecture

OpenAI · September 24, 2026

We prove the second Kahn–Kalai conjecture. For every finite simple graph H with h ≥ 1 edges and at most n vertices, the threshold for \(G(n,p)\) to contain an ordinary copy of H is at most \(C p_{\mathrm E}(n,H)(1+\log_2 h)\), where C is universal. Here \(p_{\mathrm E}(n,H)\) is the least density at which every subgraph of H has expected copy count at least one half.

Read PDF Download Source

Cite

@misc{OAI:The-second-Kahn-Kalai-conjecture-September-24-2026,
  author = {{OpenAI}},
  title = {{The second Kahn--Kalai conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf}{OAI:The-second-Kahn-Kalai-conjecture-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

The second Kahn–Kalai conjecture

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

Scope note on GitHub →