Formalizing Flag Algebras in Lean
The research formalizes Razborov's flag algebra method in Lean 4 to prove asymptotic density inequalities in extremal graph theory. It builds a system that connects abstract algebraic conditions to concrete graph properties, using semidefinite programming for certificates and a compiler to turn those certificates into verified proofs. This framework also yields new structural results about forbidden subgraphs.