Erdős Problem #71

Is it true that for every infinite arithmetic progression \(P\) which contains even numbers there is some constant \(c=c(P)\) such that every graph with average degree at least \(c\) contains a cycle whose length is in \(P\)? In [Er82e] Erdős credits this conjecture to himself and Burr. This has been proved by Bollobás [Bo77]. The best dependence of the constant \(c(P)\) is unknown. The infinite arithmetic progression is encoded as a set \(P \subseteq \mathbb{N}\) satisfying `P.IsAPOfLength ⊤` (which forces a positive common difference), and "contains even numbers" as the existence of an even element. The average degree of a finite simple graph is `SimpleGraph.averageDegree`, i.e. \((\sum_v \deg v)/|V| \in \mathbb{Q}\), and a cycle whose length is in \(P\) is a cycle walk `w` with `w.length ∈ P`.