---

Submission note. Posted to erdosproblems.com as a proof claim by Yicheng Pan (潘奕成) (account yichengpan) on 5 October 2026, giving "OpenAI ChatGPT and Codex; substantial assistance. Exact model versions were not fully recorded." as the AI used:

This proves the all-n version of the first question of #883. For every n and A subset of {1,...,n} with |A| > floor(n/2)+floor(n/3)-floor(n/6), the induced coprime graph contains a simple cycle of every odd length l satisfying 3 <= l <= floor(n/3)+1. Building on Donald Della Pietra's asymptotic framework, the proof combines an explicit analytic range n >= 200000 with exact interval certificates covering every n < 200000. An elementary odd-triple argument supplies coprime endpoints; surplus smoothing, totient profiles, prime-signature ordering and an ordered Hall argument yield the cycles. The second question is outside this contribution. Notes: The earlier claim by Donald Della Pietra proves the asymptotic result; this submission establishes the literal all-n statement used by the canonical Lean target and explicitly credits his core construction. All 6,831 local modules were independently rebuilt from unchanged frozen source with Lean 4.33.1 and pinned dependencies. The canonical raw-statement harness passed; the final theorem has only propext, Classical.choice and Quot.sound as axioms. The rebuilt final object hash matches the submitted record. One module required an 8192 MiB cap rather than the original 4096 MiB; reproduction errata are included. Public audit records: https://github.com/zoahdev/erdos883-first-question/tree/b39ee2d5711a343e3117e0ba71fdcdbcb79fc51d/audit AI tools were substantially involved. This summary was drafted with AI assistance for the author's review before submission. No independent human expert review, worldwide priority, expert endorsement or journal acceptance is claimed.

The claim. For every $n$ and every $A\subseteq\{1,\ldots,n\}$ with $|A|>\lfloor n/2\rfloor+\lfloor n/3\rfloor-\lfloor n/6\rfloor$, the coprime graph $G(A)$ contains a simple cycle of every odd length $\ell$ with $3\le\ell\le\lfloor n/3\rfloor+1$, which for odd $\ell$ is the same as $\ell\le n/3+1$ (Yicheng Pan, manuscript of 5 October 2026 in the repository zoahdev/erdos883-first-question at the pinned commit, submitted to the site's proof-claims tab the same day). The author's summary says the proof keeps the asymptotic approach of Della Pietra's claim, treats $n\ge200000$ by an analytic argument and every smaller $n$ by exact certificates over intervals, obtains coprime endpoints from an elementary argument on triples of odd integers, and builds the cycles by ordering the odd members by their totient ratios and prime signatures and applying a Hall-type matching. The tab records the claim as made using OpenAI ChatGPT and Codex, with substantial assistance and the exact model versions not fully recorded; the submission's notes say that AI tools were substantially involved and that no independent review, priority, endorsement or journal acceptance is claimed. This is the first question of Problem 883 under its literal all-$n$ reading.

The formalization. The repository's lean/ folder, at the pinned commit, names Erdos883Verified.erdos883_firstQuestion in Erdos883VerifiedCoverage.lean as the canonical statement, under Lean 4.33.1; its README reports an independent rebuild, with kernel rechecks, of all 6,831 of the project's own modules, Mathlib being taken from its pinned cache, and the axioms propext, Classical.choice and Quot.sound for the final theorem. Those are the repository's own statements: no build, audit or kernel check of the development is recorded in this corpus, and the formal statement was not compared with the problem's wording.

Covers. The first question for every $n\ge1$, all odd cycle lengths from $3$ to $\lfloor n/3\rfloor+1$: the part odd_cycles of the problem, as printed. Not covered: the second question, on complete tripartite subgraphs $K(1,\ell,\ell)$, which the author places outside the contribution and which Sárközy's Theorem 1 settles.

Depends on. Nothing in this wiki as a premise: the claim names Della Pietra's work as its framework, not as an input statement, and proves the large-$n$ range itself.

Standing. Claimed. No review of the proof is recorded in the thread; the site labels the problem OPEN, and no referee, named reviewer or independent build is recorded, so the page lists no evidence.