Skip to content

Erdős problem 71

Is it true that for every infinite arithmetic progression PP which contains even numbers there is some constant c=c(P)c=c(P) such that every graph with average degree at least cc contains a cycle whose length is in PP?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/71.lean

Formal Conjectures

FormalConjectures/ErdosProblems/71.leanErdos71.erdos_717 linesExact file
True ↔  ∀ (P : Set ℕ),    P.IsAPOfLength ⊤ →      (∃ n ∈ P, Even n) →        ∃ c,          ∀ (V : Type) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj],            c ≤ G.averageDegree → ∃ v w, w.IsCycle ∧ w.length ∈ P
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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:71

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • Formalization

    Erdős AI contributions wiki · 24 May, 2026

    Machine
    Aristotle, Claude Opus 4.7, GPT-5.5
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page