Papers With

← All papers
First page of Local flag algebras

Local flag algebras

Eoin Davey, Eoin Hurley, Rémi de Joannis de Verclos, Ross J. Kang, Jan Volec

math.CO Jul 14, 2026 · v1 cs.DM
formalization combinatorics ai-agents
Read PDF arXiv abstract Code
TL;DR
The local flag algebra framework, all four main theorems, and the rationalised SDP certificates are formalised and verified in Lean 4, partly with an agentic AI system.
Abstract
We introduce local flag algebras, a variant of Razborov's flag algebra framework in which densities are normalised by the maximum degree $Δ(G)$ rather than the order $|G|$. The framework supports the same semidefinite-method machinery as the classical version, but is tailored to extremal problems that scale with the maximum degree. As an illustrative first application we bound the number of pentagons in a triangle-free graph $G$ as a function of $|G|$ and $Δ(G)$.
Problem

Razborov's flag algebras normalise densities by graph order, which does not suit extremal problems that scale with maximum degree. A bounded-degree refinement of Erdős's pentagon problem asks for the maximum number of induced pentagons in a triangle-free graph as a function of |G| and Δ(G).

Approach

The authors define local flag algebras, in which densities are normalised by binomial coefficients in Δ(G). The framework keeps the flag product, limit functionals, averaging operator, positivity cone and weak duality, and adds a transfer principle from asymptotic to unconditional bounds. SDP certificates of size 5 and size 8 are generated by a Rust tool and rationalised into Lean source. The framework, the theorems and the certificates are formalised in Lean 4, and an agentic AI system was used to help with the formal verification and with two auxiliary theorems.

Results

The bounds P(G) ≤ |G|Δ(G)^4/40 and P(G) ≤ 0.02073·|G|Δ(G)^4 are proved. The conjectured optimum of 12/625, attained by blowups of the Clebsch graph, is established at maximum degree five. The size-5 certificate is checked entirely in Lean with no domain axioms, and a repository maps each result to its Lean statement and the axioms it depends on.