Formalizing Flag Algebras in Lean.

arXiv:2607.23500v2 Announce Type: replace-cross Abstract: Razborov's flag algebra method is one of the most successful tools for proving asymptotic density inequalities in extremal graph theory. It reduces an inequality about all large graphs avoiding a forbid