∑math20

Combinatorics · Result 184

Correspondence coloring with a fixed forbidden subgraph

2 papersLean

Proves the Alon–Krivelevich–Sudakov coloring conjecture in correspondence-coloring form: graphs avoiding any fixed subgraph F need \(O_F(\Delta/\log\Delta)\) colors when their maximum degree Δ is sufficiently large. Also proves the Ajtai–Erdős–Komlós–Szemerédi independence conjecture: for fixed r ≥ 4, every n-vertex Kr-free graph of average degree d ≥ 2 has an independent set of size \(\Omega_r(n\log d/d)\).

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 2

First page of Correspondence coloring graphs with a forbidden clique

Correspondence coloring graphs with a forbidden clique

OpenAI · October 5, 2026

For every fixed integer r ≥ 4, we prove that every Kr-free graph of sufficiently large maximum degree Δ has correspondence chromatic number \(O_r(\Delta/\log\Delta)\). This resolves the Alon–Krivelevich–Sudakov coloring conjecture in the stronger correspondence-coloring form. The same bound, with a constant depending on F, holds when any fixed graph F is excluded as an ordinary subgraph. Ordinary and list coloring satisfy the same bounds.

Read PDF Download Source

Cite
@misc{OAI:Correspondence-Coloring-Graphs-with-a-Forbidden-Clique-October-5-2026,
  author = {{OpenAI}},
  title = {{Correspondence coloring graphs with a forbidden clique}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Correspondence-Coloring-Graphs-with-a-Forbidden-Clique-October-5-2026/correspondence-coloring-forbidden-clique.pdf}{OAI:Correspondence-Coloring-Graphs-with-a-Forbidden-Clique-October-5-2026}},
  year = {2026}
}
First page of A logarithmic independence bound for clique-free graphs

A logarithmic independence bound for clique-free graphs

OpenAI · September 25, 2026

For every fixed integer r ≥ 4, every Kr-free graph on n vertices with average degree d ≥ 2 has an independent set of size at least \(c_r n\log d/d\), where \(c_r\gt 0\) depends only on r. This proves the fixed-clique-size independence conjecture of Ajtai, Erdős, Komlós and Szemerédi.

Read PDF Download Source

Cite
@misc{OAI:A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026,
  author = {{OpenAI}},
  title = {{A logarithmic independence bound for clique-free graphs}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026/paper.pdf}{OAI:A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

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

ResultComparator statement
Logarithmic independence bound for clique-free graphsCliqueFreeLog.lean

Scope note on GitHub →