arXiv++ Combinatorics

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.

Goodman proved a lower bound on triangle counts which, in graphon language, states that every graphon of edge density $p$ has triangle density at least $2p^2-p$. Bennett, Dudek, Lidický, and Pikhurko established the corresponding bound for $C_5$, determining its minimum density at every Turán density $p=1-1/k$ with an integer $k\ge3$. We extend this bound to every odd cycle in the dense regime: for every odd integer $m\ge3$ and every graphon $W$ with edge density $p\ge2/3$, $t(C_m, W) \ge p^m-p(1-p)^{m-1}.$ For $2/3\le p<1$, equality holds precisely for balanced complete $k$-partite graphons with an integer $k\ge3$, up to graphon equivalence, and we establish qualitative stability at these densities. In the same density range, we also strengthen Kim and Lee's density-sensitive commonality inequality for odd cycles by adding the nonnegative term $t(P_{m-1},1-W)-(1-p)^{m-1}$ to the lower bound, where $P_{m-1}$ is the path with $m-1$ edges. To prove the main results, we develop a spectral excursion expansion and use Dirichlet averaging to reduce the resulting polynomial inequalities in arbitrarily many spectral variables to a one-variable problem. We prove the one-variable inequality through a uniform inequality comparing odd and even moments of shifted Gamma random variables. We also formalise the odd-cycle lower-bound theorem in Lean 4.

We prove that the Turán density of the tetrahedron $K_4^{(3)}$ satisfies $π(K_4^{(3)}) \le 14993367693127837/26880000000000000 < 0.557789$, improving Baber's upper bound of $0.5615$ and closing about $62\%$ of the gap to the conjectured value $5/9$. The proof uses an exact seven-vertex flag-algebra certificate incorporating degree-stationarity from Razborov's differential method. To find the certificate, we combine the established techniques of cutting planes and column generation to optimize jointly over flag families whose types have at most five vertices. We give a complete formal proof of this Turán density bound in Lean 4.

Let $H$ be a fixed $d$-regular graph with $d\ge2$, and let $t(H,\cdot)$ denote its homomorphism density. We study the upper-tail event $t(H,G(n,p))\ge r^{|E(H)|}$ for fixed $0<p<r<1$ in a dense Erdős--Rényi random graph $G(n,p)$. Near the Lubetzky--Zhao replica-symmetric phase boundary and away from the exceptional target density $(d-1)/d$, we prove that the optimizer of the Chatterjee--Varadhan variational problem on the symmetry-breaking side is bipodal (two-block) and unique up to relabeling. Its block parameters depend analytically on $(p,r)$. To treat the exceptional boundary point, where the nonexceptional theory degenerates, we construct an analytic curve approaching that point from the symmetry-breaking side along which the unique optimizers are nonconstant rank-one bipodal graphons. In both settings, we derive asymptotic expansions of the edge-density deficit and the rate function that governs the exponential decay of the upper-tail probability. Moreover, the conditioned random graph converges in cut distance to the corresponding bipodal optimizer as $n\to\infty$. As $(p,r)$ approaches the phase boundary from the symmetry-breaking side, the optimizers converge to their constant limits through two distinct mechanisms. For each fixed nonexceptional target density, one block shrinks to zero measure, giving convergence in $L^1$ but not in $L^\infty$. Along the exceptional curve, both blocks remain macroscopic: their sizes tend to $1/2$ and all three block densities tend to $(d-1)/d$, yielding convergence in $L^\infty$.

Algebraic combinatorics often seeks bijections that explain identities between distributions object by object. Encoding combinatorial objects as words lets automata theory study such a bijection as a word-to-word computation and measure its memory, input access, and control of output order. This refines existence questions by asking which computational mechanisms a bijection requires. We develop this viewpoint for Dyck paths. Our motivating example is the $q,t$-Catalan polynomial. Let $D_n$ be the set of Dyck paths of semilength $n$, let $D=\bigcup_{n\ge 0}D_n$, and let $area, dinv, bounce \colon D\to\mathbb{N}$ be the standard statistics. Then, \[ C_n(q,t)=\sum_{P\in D_n}q^{area(P)}t^{bounce(P)} =\sum_{P\in D_n}q^{dinv(P)}t^{area(P)}. \] Haglund's zeta map $ζ\colon D\to D$ gives a bijective proof: it preserves semilength and sends $(dinv,area)$ to $(area,bounce)$. By contrast, the full symmetry $C_n(q,t)=C_n(t,q)$ still lacks a direct explanation: no explicit, uniform, semilength-preserving bijection is known that swaps area and dinv on every Dyck path. Polyregular maps from automata theory provide a natural computational starting point, but we prove that neither $ζ$ nor the classical height-sweep bijection witnessing Narayana symmetry is polyregular. The missing mechanism is global ordering by numerical levels whose range grows with the input. We call this a \emph{rank sort} and introduce \emph{weighted-rank polyregular maps} (WRP), extending polyregular maps by one such sort and containing both bijections. Nevertheless, WRP is a proper subclass of deterministic logspace. We prove that $ζ^{-1}$ lies outside WRP and that no WRP map can realise a semilength-preserving area-dinv swap. Thus the rank-sorting strategy behind $ζ$ cannot be extended within WRP to exchange the two statistics.

Razborov's flag algebra forms a powerful framework for deriving asymptotic inequalities between induced subgraph densities, underpinning many advances in extremal graph theory. This survey introduces flag algebra to computer scientists working in logic, programming languages, automated verification, and formal methods. We take a logical perspective on flag algebra and present it in terms of syntax, semantics, and proof strategies, in a style closer to formal logic. One popular proof strategy derives valid inequalities by first proving inequalities in a labelled variant of flag algebra and then transferring them to the original unlabelled setting using the so-called downward operator. We explain this strategy in detail and highlight that its transfer mechanism relies on the notion of what we call an adjoint pair, reminiscent of Galois connections and categorical adjunctions, which appear frequently in work on automated verification and programming languages. Along the way, we work through representative examples, including Mantel's theorem and Goodman's bound on Ramsey multiplicity, to illustrate how mathematical arguments can be carried out symbolically in the flag algebra framework.