{"id":"palomar/PALOMAR-2026-10-18-000002","url":"https://github.com/jtraverso/graph-removal-lemma/tree/589cf03ef1e4c80ea8cdd6be77778232c62dd37c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000002-v1.json","repo":"https://github.com/jtraverso/graph-removal-lemma","tags":["math.CO","msc:05C35","extremal-graph-theory","removal-lemma","lean"],"score":0,"title":"The graph removal lemma for every fixed graph","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the graph removal lemma of Erdős, Frankl and Rödl for an arbitrary fixed finite graph H on k vertices: for every ε > 0 there is δ > 0, depending only on H and ε, such that every finite graph on n vertices with fewer than δ nᵏ labelled copies of H can be made H-free by deleting fewer than ε n² edges; equivalently (far form), a graph from which at least ε n² edges must be deleted to destroy all copies of H has at least δ nᵏ labelled copies. Also included is the counting lemma used in the proof: if parts s x (one for each vertex x of H) are robustly dense…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"The asymptotic number of graphs not containing a fixed subgraph and a problem for hypergraphs having no exponent","identifier":"doi:10.1007/BF01788085","relationship":"formalizes"}]}