{"id":"arxiv/2607.23500","url":"https://arxiv.org/abs/2607.23500","tags":["cs.LO","cs.AI","cs.PL","math.CO"],"score":0,"title":"Formalizing Flag Algebras in Lean","domain":"cs.LO","source":"arxiv","authors":["Gyeongwon Jeong","Seonghun Park","Jihoon Hyun","Sang-il Oum","Hongseok Yang"],"reviews":0,"subject":"cs.LO","summary":"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 forbidden pattern to finitely many algebraic conditions, and a certificate satisfying them can be found by semidefinite programming. We formalize the method for finite simple graphs in Lean 4, building on Mathlib. The formalization covers flags and their densities, the flag algebra as a quotient vector space, positive homomorphisms as limits of graph sequences, Razborov's random extensions, and the…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-26","reactions":{}}