Seonghun Park (박성훈), Formalizing Flag Algebras in the Lean Theorem Prover
Flag algebras are a mathematical framework introduced by Alexander Razborov in 2007, which has been used to resolve a wide range of open problems in extremal graph theory in the past twenty years. This framework provides an algebraic setup where one can express relationships between induced subgraph densities symbolically. It also comes with mathematical techniques …