Erdős problem 180
For every finite family of graphs, is there a single with ? A counterexample refutes the Erdős-Simonovits compactness conjecture.
Sources
FormalConjectures/ErdosProblems/
180.lean
Retained formal statement
If is a finite set of finite graphs then is the maximum number of edges a graph on vertices can have without containing any subgraphs from . Note that it is trivial that for every . Is it true that, for every , there exists such that
This is the Erdős–Simonovits compactness conjecture. The answer is no: OpenAI [OpenAI26] give a family of connected bipartite graphs, none of them acyclic, for which no single member controls the family extremal number. See erdos_180.variants.counterexample.
False ↔ ∀ (family : Finset Erdos180.FiniteGraph), family.Nonempty → Erdos180.IsCyclicFamily family → Erdos180.IsCompactFamily familySolvedStatement only, no proof