Erdős problem 150
A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let be the maximum number of minimal cuts a graph on vertices can have.
Sources
FormalConjectures/ErdosProblems/
150.lean
A minimal cut of a graph is a minimal set of vertices whose removal disconnects the graph. Let be the maximum number of minimal cuts a graph on vertices can have.
Does for some ?
It is unclear in [Er88] whether Erdős knew that the limit existed, which follows from a simple argument first given in the literature (to the best of my knowledge) by Bradač [Br24].
That was proved by Fomin, Kratsch, Todinca, and Villanger [FKTV08], who proved . This was independently studied by Bradač [Br24] (unaware of this earlier work), who proved that , where is the binary entropy function.
True ↔ ∃ α < 2, Filter.Tendsto (fun n => ↑(Erdos150.maxMinimalCuts n) ^ (1 / ↑n)) Filter.atTop (nhds α)