Formalizing Flag Algebras in Lean
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 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 downward operator that averages out labels. On top of this theory, we build verified computation of flag densities and a tactic that turns certificates found by semidefinite programming into Lean proofs. The certificate serves only as candidate data; Lean checks every fact the proof uses. With this development we verify seven Turán-type upper bounds. Adding lower-bound constructions proved in Lean yields the asymptotic form of Mantel's theorem and the asymptotic Erdős pentagon theorem π(C5;K3)=24/625; to our knowledge, the latter has not previously been formalized in a proof assistant. We also prove two inequalities of Goodman. All density theorems reported here depend only on the standard axioms of Lean's logic. Formalization also led us to treat forbidden subgraphs with a different semantics. Instead of building a separate flag algebra for each forbidden family, we keep a single algebra of all graphs and impose the constraint only when interpreting an inequality, through randomly labeled limits of graphs satisfying it. We prove that this ensemble semantics yields the intended density bounds, and that a condition we call root-plantability characterizes when it agrees with the standard semantics.
Related
- Formalizing Fefferman's Official Periodic Navier-Stokes Problem (B) in Lean 4: Global Linear Strain Exclusion on T3, Biot-Savart Direction Depletion Identities, and Conditional Reductions via Beale-Kato-Majda
- Formalizing Carleson's Theorem in Lean
- Commuting Families of Flag Quasideterminants in Reflection Equation Algebras of Type A
- Vertex Operator Algebras in Lean: a formal library and its companion book
- A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras
BibTeX
@misc{jeong2026formalizing,
title = {{Formalizing Flag Algebras in Lean}},
author = {Gyeongwon Jeong and Seonghun Park and Jihoon Hyun and Sang-il Oum and Hongseok Yang},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2607.23500},
eprint = {2607.23500},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2607.23500},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Formalizing Flag Algebras in Lean
AU - Gyeongwon Jeong
AU - Seonghun Park
AU - Jihoon Hyun
AU - Sang-il Oum
AU - Hongseok Yang
PY - 2026
DA - 2026/10/14
PB - arXiv
DO - 10.48550/arxiv.2607.23500
UR - https://arxiv.org/abs/2607.23500
AB - 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 downward operator that averages out labels. On top of this theory, we build verified computation of flag densities and a tactic that turns certificates found by semidefinite programming into Lean proofs. The certificate serves only as candidate data; Lean checks every fact the proof uses. With this development we verify seven Turán-type upper bounds. Adding lower-bound constructions proved in Lean yields the asymptotic form of Mantel's theorem and the asymptotic Erdős pentagon theorem π(C_5;K_3)=24/625; to our knowledge, the latter has not previously been formalized in a proof assistant. We also prove two inequalities of Goodman. All density theorems reported here depend only on the standard axioms of Lean's logic. Formalization also led us to treat forbidden subgraphs with a different semantics. Instead of building a separate flag algebra for each forbidden family, we keep a single algebra of all graphs and impose the constraint only when interpreting an inequality, through randomly labeled limits of graphs satisfying it. We prove that this ensemble semantics yields the intended density bounds, and that a condition we call root-plantability characterizes when it agrees with the standard semantics.
ER -