---

Claim. Haoyu Chen, Explicit upper bounds for the Erdős–Surányi function $g(n)$, a Zenodo record whose concept DOI resolves to its latest version (version 14, 8 September 2026, the version the claim's summary describes; CC0). Submitted to the proof-claim tab of Problem 708 on 2026-09-05 as a partial claim, at the moderator's request in place of per-version comments. The results, as the summary and the repository state them: $g(n)\le12n$ for every $n\ge1$ (Theorem 17.1 of version 14), with a Lean 4 development the author reports kernel-checked; $g(n)\le11n$ by an argument in the paper that is not formalized; and the conjectured bound $g(n)\le2n$ whenever $\max(A)\ge8n^3$. The convention is the at-most one of the problem page's Progress section: the formal statement asks, for every $n\ge1$, every set $A$ of $n$ integers at least $2$ and every natural number $x$, for some $B\subseteq\{x+1,\ldots,x+\max A\}$ with $\lvert B\rvert\le12n$ (or the bound in question) and $\prod_{a\in A}a\mid\prod_{b\in B}b$, so the intervals lie in the positive integers, the 1992 domain. The method, by the summary: a linear-programming duality reduces a linear bound to a single inequality for weighted counts of prime factors over intervals, which is proved from explicit counting certificates checked by decide. The statements above come from the claim's summary, the record page and the repository's README.

Submission note. Posted to erdosproblems.com as a proof claim by Haoyu Chen (account chenhaoyu) on 5 September 2026, giving "GPT-5.6 Sol (ChatGPT Pro) and Claude (Fable 5.1 / Opus) for proof search and refereeing; every proof re-verified by scripts in the linked repository" as the AI used:

Partial result: explicit upper bounds for g(n), not a resolution of the (2+o(1))n question. Main result of the linked paper (v14): g(n) <= 12n for all n. This bound is kernel-verified in Lean 4 (v4.34.0-rc1, Mathlib de5ce8a9); the final theorem depends only on propext, Classical.choice and Quot.sound. Also in the paper: g(n) <= 11n (refereed, not formalised), and the conjectured 2n holds whenever max(A) >= 8n^3. Method: an LP duality reduces a linear bound to a 'hinge inequality' for weighted prime-factor counts on intervals, which is proved by explicit counting certificates checked by decide. Notes: The link is a Zenodo concept DOI and always resolves to the latest version of the paper (currently v10; the record's changelog lists the version history). Paper source, verification scripts and engine transcripts: https://github.com/chy4pro/erdos-708-explicit-upper-bounds . Submitted at the moderator's request in place of per-version comments.

Covers. A finite explicit upper bound in the at-most convention, $g_{\le}(n)\le12n$ for all $n$ and intervals of positive integers (the 1992 domain), and the conjectured bound $2n$ for the sets with $\max(A)\ge8n^3$. Not covered: the displayed questions $g(n)\le(2+o(1))n$ and $g(n)\le2n$ for all sets, which the claimant says remain open; intervals of arbitrary consecutive integers, which the claim does not state; and the displayed exact-size formulation $\lvert B\rvert=g(n)$, which the claim does not address.

Formalization. The repository chy4pro/erdos-708-explicit-upper-bounds at the pinned commit of 25 September 2026 (a privacy edit of transcripts and scripts after the mathematics of 8 September) holds the development under lean/ on the Lean toolchain and Mathlib revision its Lean README pins. That README names Erdos708Final.g_le_81n in Erdos708/Final.lean as the kernel-verified final theorem and tabulates the later bounds, Erdos708H17.g_le_33n (Theorem 15.1), Erdos708Chain19.g_le_19n (Theorem 16.1) and Erdos708H97.g_le_12n in Erdos708/H97/Chain.lean (Theorem 17.1), with the statement that only propext, Classical.choice and Quot.sound are used and no sorry, admit, native_decide or custom axiom occurs; a check script FinalCheck.lean is said to succeed silently. Nothing was built, replayed or audited in this corpus, and the statement's fidelity to the problem was not examined beyond the README's informal rendering.

History. The author's comment of 7 September 2026 on the claim reported version 11, in which the bound $g(n)\le81n$ was extended from $n\le10^{962}$ to all $n$ by a divisor certificate with coefficients of both signs, with a formalization in progress. The record's version history then lists the formalization (version 12), $g(n)\le33n$ kernel-verified (version 13, 7 September) and $g(n)\le12n$ kernel-verified (version 14, 8 September). The claim's tools line names GPT-5.6 Sol (ChatGPT Pro) and Claude (Fable 5.1 / Opus) for proof search and refereeing, with every proof re-verified by scripts in the repository, and the author's comment of 7 September names GPT-6 Astra as the finder and Claude Opus 5 as the referee of the version 11 proof; the summary's word refereed for the $11n$ bound refers to those automated referee runs, not to a journal.

Acceptance. None. The site's label is OPEN and its commentary does not mention the claim; the claim's only comment is the author's own update; no curator, journal or outside expert review exists, and the Lean development was not built here. The claim enters as claimed, and as a partial claim it does not change the problem's standing.

Depends on. No page of this wiki.