Open Research Index

Formalizing Flag Algebras in Lean

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

arXivarxiv/2607.23500Jul 26, 2026cs.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2607.23500
curl -X POST /api/v1/records/arxiv/2607.23500/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.23500/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'