---

Claim. Every finite graph with minimum degree at least $4$ and diameter at most $3$ contains a cycle of length $4$ or $8$. The proof, posted by Murat Can Temeller as issue 1 of the zey9310/zey9310-math repository on 2 October 2026 (the claim's date) and registered the same day on the site's proof-claims tab, extends Carr's theorem that every graph of diameter $2$ and minimum degree at least $3$ contains a $4$- or $8$-cycle (arXiv:2508.19302) to diameter $3$, at the cost of raising the minimum degree to $4$. Suppose there is no $4$-cycle and no $8$-cycle, so two vertices share at most one neighbor and every edge lies in at most one triangle. If every edge lies in a triangle, a shortest path between outer neighbors of two neighbors of a fixed vertex, lengthened by detours through the triangles at that vertex, gives an $8$-cycle. Otherwise an edge $uv$ in no triangle is fixed; the other neighbors $A$ of $u$ and $B$ of $v$ are disjoint with no edges between them, their further neighbors are distributed by a bridge argument and a funneling lemma, and the diameter bound forces short connections between a child of $A$ and a child of $B$ that in every case close a $4$- or $8$-cycle. Read depth: the issue in full; this corpus has not checked the argument. The author credits the theorem, proof and computations to Claude Opus 5.5 (Anthropic), the system the submission names, in a session the author directed, and reports exhaustive SAT-modulo-symmetries searches, checked against nauty, finding no graph of minimum degree at least $4$, diameter at most $3$ and no $4$- or $8$-cycle on $13$ to $30$ vertices, and none with all degrees in $\{3,4\}$ on $24$ to $30$ vertices.

Submission note. Posted to erdosproblems.com as a proof claim by Murat Can Temeller (account murican) on 2 October 2026, giving "Claude Opus 5.5 (Anthropic)" as the AI used:

Shows that every graph with minimum degree at least 4 and diameter at most 3 contains a cycle of length 4 or 8, so the conjecture holds for these graphs. This extends Carr's diameter-2 result to diameter 3 for minimum degree ≥ 4. The proof splits into two cases: if every edge lies in a triangle, detours through triangles force an 8-cycle; otherwise a case analysis around an edge in no triangle (bridges, a funnelling lemma, and the short connections forced by the diameter) produces a 4-cycle or an 8-cycle. Notes: The theorem, proof and computations were produced by Claude Opus 5.5 (Anthropic) in a session I directed. The proof has been checked step by step but not yet independently verified by a human expert; review is very welcome, especially Case 1 and Step 4a. Exhaustive SAT Modulo Symmetries searches (following Balaji's pipeline, validated against nauty) find no counterexample on 13 to 30 vertices, and nauty independently reproduces the positive-control counts. Separately, no graph with all degrees in {3, 4} and diameter at most 3 avoids both 4- and 8-cycles on 24 to 30 vertices. What remains open for diameter 3 is graphs with vertices of degree 3. Full proof, code and logs are at the link.

Covers. The statement of Problem 64 for graphs of minimum degree at least $4$ and diameter at most $3$, where the cycle found has length $2^2$ or $2^3$. Graphs of diameter at most $3$ with a vertex of degree $3$ are not covered, and the author names them as the remaining gap for diameter $3$.

Depends on. Nothing in this wiki; the argument is self-contained apart from Carr's theorem, which it extends rather than uses.

Standing. Claimed: when read the proof was posted only as the issue text, the submission's formalization link pointed to the same issue and no Lean or other machine-checked proof was known to this corpus, and the author says the proof has been checked step by step but not by an independent expert. The two comments on the site's claim (2 and 3 October 2026) ask about that disclaimer and receive the author's reply that they are not an expert; one comment on the issue (5 October) suggests formalizing it. The computational searches are author-reported, and this corpus has not replayed them.