Invited Talk by Hongseok Yang (KAIST, Korea): Introduction to Razborov's Flag Algebras: Logic-Based Computational Methods in Extremal Combinatorics

A few years ago, during a sabbatical visit to a discrete mathematics group, I was encouraged by experts in combinatorics to study Razborov’s flag algebras. They highlighted the power of the flag algebras as a computational method for solving problems in extremal combinatorics — a field where the flag algebras have yielded some of the best-known results for undirected graphs, directed graphs, hypergraphs, and permutations. They also explained that the flag algebras had deep connections to logic and optimisation, encoding finite combinatorial objects and constraints as finite structures and universally-quantified formulas, and exploiting semidefinite programming to generate bounds in extremal combinatorics automatically. They conjectured that the flag algebras could suggest effective ways to use logic, programming languages, and machine learning for generating mathematical results automatically.

In this talk, I will describe what I have learnt by following this recommendation for about a year. My goal is to introduce the key ideas behind the flag algebras and their achievements in a way that is accessible to a non-expert audience in logic and computer science. If time permits, I will also discuss our ongoing work on formalising the flag algebras in the Lean theorem prover.