🔢 mathematics

Formalizing Flag Algebras in Lean

This paper presents a machine-checked formalization of Razborov's flag algebra method in Lean, featuring a compiler that independently verifies semidefinite programming certificates to rigorously prove seven Turán-type upper bounds and explore the meta-theoretic nuances of imposing graph constraints.

Original authors: Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang

Published 2026-07-28

📖 3 min read🧠 Deep dive

CC BY 4.0

Original authors: Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a detective trying to solve a mystery about how things fit together. In the world of math, specifically a branch called "extremal graph theory," the mystery is this: If you have a huge collection of dots (vertices) connected by lines (edges), and you are strictly forbidden from drawing a specific shape—like a triangle or a square—what is the absolute maximum number of lines you can draw before you accidentally create that forbidden shape? It's like trying to pack as many toys as possible into a box without crushing a fragile vase in the middle. Mathematicians have been trying to find these "packing limits" for decades, but the numbers get so huge and the patterns so complex that human brains can't check every single possibility.

To tackle this, mathematicians invented a clever trick called "flag algebras." Think of a "flag" not as a piece of cloth on a pole, but as a tiny, labeled snapshot of a graph. If you have a giant graph, a flag is just a small piece of it where some dots are marked with stickers (labels) to keep track of who is who. The method uses these tiny snapshots to write down algebraic equations that describe the whole giant graph. It's like trying to understand the weather of an entire continent by measuring the wind speed in just a few specific, labeled spots. By solving these equations, mathematicians can prove strict upper limits on how many lines can exist without breaking the rules. However, these proofs often rely on massive computer calculations that are too big for a human to double-check by hand, leaving a nagging doubt: "Did the computer make a mistake?"

This paper is about building a super-strict, machine-checked safety net for these proofs. The authors, a team of researchers from Korea, have translated the entire theory of flag algebras into a programming language called Lean, which acts like a hyper-logical robot judge. They didn't just write the rules; they built a "certificate-to-proof compiler." Imagine a scenario where a computer program (like a detective's assistant) finds a solution and hands you a stack of papers claiming, "Here is the proof!" Usually, you'd have to trust that the computer didn't mess up the math. But this paper introduces a system where the computer's stack of papers is treated as a suspect. The Lean compiler takes that stack, re-does every single calculation from scratch using its own internal logic, checks that the computer's "positive semidefinite matrices" (a fancy way of saying "guaranteed non-negative numbers") are actually correct, and then assembles a final, unbreakable proof.

The team tested this system on seven famous mathematical puzzles, including Mantel's theorem (about triangle-free graphs) and the Erdős pentagon theorem (about pentagons in triangle-free graphs). They successfully turned external computer-generated "certificates" into formal, machine-verified proofs for all seven cases. This means that for these specific problems, we now have a mathematical guarantee that the answers are correct, down to the last decimal, because a computer has verified every step of the logic. They also used their new tools to prove some lower bounds (showing that you can reach these limits) and explored a deep theoretical question about how to handle the "forbidden" shapes in the math, discovering that sometimes the way you set up the rules matters more than you think. Ultimately, this work doesn't just solve a few old riddles; it builds a new, reliable engine that can take complex, computer-assisted math and turn it into ironclad, human-verifiable truth.

Technical Summary: Formalizing Flag Algebras in Lean

Problem Statement

Extremal graph theory frequently addresses questions regarding the maximum frequency of a specific finite pattern $F$ in graphs that avoid a set of forbidden patterns $H$ . Determining the asymptotic Turán density $\pi(F; H)$ is notoriously difficult because it requires controlling the behavior of all sufficiently large $H$ -free graphs. Razborov's flag algebra method provides a powerful technique for this setting, reducing the proof of asymptotic bounds to checking finitely many algebraic conditions via semidefinite programming (SDP).

However, the practical application of this method relies on "candidate certificates" generated by external SDP solvers (e.g., Flagmatic). These certificates consist of thousands of exact density values and rational positive-semidefinite (PSD) matrices. While mathematically sound, verifying these certificates by hand is impractical, and trusting external software without formal verification introduces a gap in the logical chain of proof. The challenge is to create a machine-checked framework that can ingest these external certificates, verify the underlying finite combinatorial data (isomorphisms, densities, products), and produce a formal proof within a proof assistant (Lean) that does not rely on the trustworthiness of the external solver or the manual transcription of data.

Methodology

The authors present a comprehensive formalization of Razborov's flag algebra method in Lean 4, structured into three distinct layers and a meta-theoretic investigation:

1. The Specification Layer (Mathematical Foundations)

This layer formalizes the abstract mathematical definitions of flag algebras for finite simple graphs, closely following the standard literature.

Definitions: It defines flag types (isomorphism classes of labeled graphs), flags, and the flag algebra $A_\sigma$ as a quotient of a free vector space by expansion identities (derived from the chain rule).
Semantics: It defines positive homomorphisms as maps from the algebra to $\mathbb{R}$ that preserve structure and non-negativity. The semantic non-negativity cone $C_\sigma$ is defined as the set of elements non-negative under all such homomorphisms.
Constrained Semantics: Unlike traditional presentations that build the forbidden-graph constraint $H$ into the algebra's construction, this formalization constructs the ambient algebra of all finite graphs. The $H$ -freeness condition is imposed later via an "ensemble semantic order." This order restricts the positive homomorphisms considered to those that assign zero density to graphs containing $H$ , using a random-extension measure to interpret inequalities on labeled flags.
Downward Operator: It formalizes the operator that maps labeled algebra elements to unlabeled ones, proving that it preserves semantic non-negativity (Theorem 2.9).

2. The Reflection Layer (Executable Computations)

Since the specification layer relies on non-computable quotient types and abstract definitions, a separate "reflection layer" is developed to perform the necessary finite calculations.

Concrete Representations: It uses concrete data structures (e.g., Sym2Graph with vertices as Fin n and edges as finite sets) to represent graphs and flags, enabling enumeration and decidable equality.
Adequacy Theorems: The core of this layer consists of theorems proving that the executable computations (density calculations, isomorphism checks, downward normalizing factors) agree with the abstract definitions in the specification layer.
Metaprogramming: Custom elaboration-time commands generate specific flags, density tables, and multiplication tables for the sizes required by a specific certificate. These commands prove completeness lemmas ensuring that all relevant isomorphism classes are covered.

3. The Certificate-to-Proof Compiler

This component automates the translation of external SDP certificates into verified Lean proofs.

Input: It accepts a JSON certificate from Flagmatic containing target graphs, forbidden graphs, proposed bounds, flag types, and rational PSD matrices.
Verification Process:
1. Re-generation: It regenerates the necessary flags and density/multiplication identities using the reflection layer, rather than trusting the certificate's data.
2. PSD Verification: It reconstructs the rational matrices and verifies their positive semidefiniteness over $\mathbb{Q}$ using exact $LDL^\top$ factorizations, avoiding floating-point arithmetic.
3. Algebraic Assembly: It uses the verified identities to expand the certificate's algebraic identity (decomposing the gap $c \cdot 1 - [F]$ into downward squares and a non-negative remainder) and checks the final inequality.
Trust Model: The compiler script is untrusted; it generates a proof proposal. Lean independently checks every step, including the matrix factorizations and the algebraic normalization. The script is only trusted for translation fidelity (mapping certificate flags to Lean's enumeration), which is auditable by inspecting the generated theorem statement.

4. Meta-Theory of Constrained Semantics

The paper investigates the relationship between the "ensemble semantics" (used in the implementation) and the "quotient semantics" (where constraints are built-in).

Root-Plantability: The authors define a criterion called "root-plantability" to characterize when the two semantic approaches agree. They prove that if a graph class is "blow-up-closed" (e.g., $K_r$ -free graphs for $r \ge 3$ ), the two orders agree.
Counterexample: They provide a counterexample ( $C_4$ -free graphs) where the orders differ, demonstrating that heredity alone is insufficient for agreement.

Key Results

The authors evaluated the compiler on seven distinct upper-bound certificates, successfully producing machine-checked proofs for:

Mantel's Theorem: Proving $\pi(K_2; K_3) = 1/2$ .
Erdős Pentagon Theorem: Proving $\pi(C_5; K_3) = 24/625$ . (No proof avoiding flag algebras is known for this result).
$C_4$ -density: An upper bound on the density of $C_4$ in triangle-free graphs.
Edge-density bounds: For $K_4$ -free, $K_5$ -free, and $C_5$ -free graphs.

Additionally, the formalization was used directly (without the compiler) to:

Prove the matching lower bounds for Mantel's theorem and the Erdős pentagon theorem using explicit constructions.
Prove two inequalities of Goodman.

All seven certificates were compiled into Lean source files containing no sorry or axioms. Five of the seven were verified entirely by kernel reduction (decide +kernel), while the two largest ( $K_5$ -free and $C_5$ -free edge density) required native decide due to computational limits, a limitation the authors explicitly acknowledge.

Significance and Claims

The paper claims to provide the first machine-checked formalization of the flag algebra method for finite simple graphs, bridging the gap between computer-assisted search and rigorous formal proof. Its significance lies in:

Verification of Complex Combinatorics: It demonstrates that flag algebra proofs, which rely on massive amounts of exact finite data and SDP results, can be fully verified in a proof assistant without trusting the external solver or manual transcription.
Modular Architecture: The separation of the specification (math), reflection (computation), and compiler (automation) layers offers a reusable framework for formalizing other extremal problems.
Meta-Theoretic Insight: The formalization of the ensemble semantics and the root-plantability criterion provides a rigorous mathematical understanding of the constraints imposed by the implementation, clarifying when the "random-label" approach is equivalent to the "built-in constraint" approach.
New Proofs: It provides the first formal proof of the Erdős pentagon theorem and new formal proofs for Goodman's inequalities and lower bounds for Turán densities.

The authors remain modest about the current limitations, noting that the approach relies on external SDP solvers for certificate discovery and that scaling beyond five vertices currently faces significant computational hurdles in kernel-checked verification. They view this work as a foundation for future extensions to hypergraphs, directed graphs, and the integration of graphon theory.