Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper formalizes Razborov's flag algebra method within the Lean proof assistant, enabling the verification of asymptotic inequalities in extremal graph theory through a machine-checked framework. The authors introduce a certificate-to-proof compiler that transforms semidefinite programming outputs into algebraic proofs, ensuring that the necessary computations are independently verified by Lean. Their formalization successfully proves seven Turán-type upper bounds, including significant results like Mantel's theorem and the Erdős pentagon theorem, while also exploring the implications of different approaches to imposing graph constraints.
Formalizing flag algebras in Lean not only secures the proofs of key extremal graph theorems but also reveals a new criterion for comparing graph constraint methods.
Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Tur\'an-type upper bounds, including Mantel's theorem and the Erd\H{o}s pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Tur\'an densities of Mantel's theorem and the Erd\H{o}s pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.