This repository contains our formalization of Brandt's proof of the Andrásfai-Erdős-Sós theorem: colorable_of_cliqueFree_lt_minDegree

If G is Kᵣ₊₁-free and (3r - 4)n/(3r - 1) < δ(G) then G is (r + 1)-colorable.

The proof of the main theorem is in AESBrandt.AES.lean

References:

B. Andrasfái, P Erdős, V. T. Sós On the connection between chromatic number, maximal clique, and minimal degree of a graph https://doi.org/10.1016/0012-365X(74)90133-2

S. Brandt On the structure of graphs with bounded clique number https://doi.org/10.1007/s00493-003-0042-z