Erdős problem 180

For every finite family $\mathcal{F}$ of graphs, is there a single $G \in \mathcal{F}$ with $\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})$ ? A counterexample refutes the Erdős-Simonovits compactness conjecture.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

180.lean

Retained formal statement2 of 2

The counterexample: a nonempty family of connected bipartite graphs, none acyclic, that is not compact.

FormalConjectures/ErdosProblems/180.leanErdos180.erdos_180.variants.counterexample4 linesExact file

1∃ family,2  family.Nonempty ∧3    (∀ forbidden ∈ family, forbidden.graph.Connected ∧ forbidden.graph.IsBipartite ∧ ¬forbidden.graph.IsAcyclic) ∧4      ¬Erdos180.IsCompactFamily family

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.