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$?

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.