Who is the author of this contribution?
Yicheng Pan (潘奕成), whose GitHub account is zoahdev and Erdős Problems account is yichengpan, is the author of the linked all-n first-question contribution. The public proof repository contains the manuscript, Lean source, rebuild audit and reproduction errata.
这项贡献的作者是潘奕成（Yicheng Pan），GitHub 账号为 zoahdev，题目网站账号为 yichengpan。贡献范围为 Erdős #883 第一问对所有自然数 n 的完成及 Lean 形式化，建立在 Donald Della Pietra 的充分大 n 结果及核心构造之上。
Exact mathematical statement
For every natural number n and every A ⊆ {1,…,n} with |A| > floor(n/2) + floor(n/3) − floor(n/6), the induced coprime graph G(A) contains a simple cycle of every odd length ℓ satisfying 3 ≤ ℓ ≤ floor(n/3) + 1.
The repository splits the proof into exact finite certificates for n < 200000 and an analytic argument for n ≥ 200000. Its final theorem is Erdos883Verified.erdos883_firstQuestion.
Contribution, prior work and review status
Donald Della Pietra's preceding asymptotic framework and core construction are explicitly credited. This contribution completes the all-n first-question statement; it does not claim to originate that asymptotic method. The second question was previously solved by Sárközy and is outside this contribution.
The author submitted a public proof claim on 5 October 2026. Listing a proof claim does not constitute the site's verification or endorsement. The repository reports a separate source rebuild of 6,831 local Lean modules and a canonical statement check. This page summarizes those published records; it does not report a new independent rebuild.
AI tools substantially assisted the work. No independent human expert review, worldwide first priority, expert endorsement or journal acceptance is claimed.
公开提交和 Lean 内核复现记录与独立专家评审属于不同证据。本站保留前人贡献、AI 协助及尚无专家认可的披露；不把整道 #883 的所有结果归于单一作者。