An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
Gyeongwon Jeong, Seonghun Park, Hongseok Yang
TL;DR
Problem: deriving asymptotic inequalities between induced subgraph densities in large graphs under forbidden patterns. Approach: a logic-inspired presentation of flag algebra with limiting graphs $\Phi$, density expressions, and a downward operator to transfer inequalities from labelled variants via adjoint pairs. Contributions: a precise syntax/semantics framework, a sound transfer lemma for the downward operator, and worked examples (e.g., Mantel's theorem and Goodman's bound) plus discussion of automation and formal-methods perspectives. Significance: enables rigorous, checkable derivations of tight asymptotic bounds in extremal graph theory and builds bridges to logic, verification, and program verification communities.
Abstract
Razborov's flag algebra forms a powerful framework for deriving asymptotic inequalities between induced subgraph densities, underpinning many advances in extremal graph theory. This survey introduces flag algebra to computer scientists working in logic, programming languages, automated verification, and formal methods. We take a logical perspective on flag algebra and present it in terms of syntax, semantics, and proof strategies, in a style closer to formal logic. One popular proof strategy derives valid inequalities by first proving inequalities in a labelled variant of flag algebra and then transferring them to the original unlabelled setting using the so-called downward operator. We explain this strategy in detail and highlight that its transfer mechanism relies on the notion of what we call an adjoint pair, reminiscent of Galois connections and categorical adjunctions, which appear frequently in work on automated verification and programming languages. Along the way, we work through representative examples, including Mantel's theorem and Goodman's bound on Ramsey multiplicity, to illustrate how mathematical arguments can be carried out symbolically in the flag algebra framework.