---

Claim. The manuscript "A proposed solution to Erdős Problem 1059: Prime avoidance for a sparse set of shifts" (5 September 2026) states as its Theorem 1 that for any function $K(X)=o(\log X)$, every sufficiently large $X$ and any $k\le K(X)$ distinct integers $h_1,\dots,h_k\in[1,X]$, some prime $p\in(2X,3X]$ has $p-h_i$ composite for every $i$. Its Corollary 1 takes $X=m!$ and the shifts $1!,2!,\dots,m!$: for every large $m$ there is a prime $p\in(2\cdot m!,3\cdot m!]$ with $p-i!$ composite for each $i\le m$, and since every $k$ with $k!<p$ then satisfies $k\le m$, these primes answer Problem 1059 in the affirmative. The argument gives one prime per interval $(2X,3X]$, so it asserts infinitude and not a positive proportion of the primes. The tab entry describes the method as an adaptation of the truncated-product construction of the OpenAI long-gaps note recorded on the release's Problem 4 page, with a coefficient estimate for primitive characters that allows averaging over primes through Vaughan's mean value theorem. This page rests on the manuscript's statements; its proof is not checked here.

Submission note. Posted to erdosproblems.com as a proof claim by Johan Land (account JohanLand) on 5 September 2026, giving "GPT-6-Astra, Fable 5.1, Gemini-3.8-Flash" as the AI used:

Astra/Fabel-5.1/Gemini-Flash-3.8 working inside a specialized ~3m lean repo for fast proof search. The stronger claim is: for any prescribed (K(X)=o(\log X)), every sufficiently large (X), and any (k\le K(X)) distinct shifts (h_i\in[1,X]), some prime (p\in(2X,3X]) makes every (p-h_i) composite. Taking (X=m!) and (h_i=i!) yields #1059. The proof adapts the truncated-product framework from OpenAI’s Improved long gaps between primes, adding a primitive-character coefficient estimate to permit prime averaging via Vaughan’s theorem. Formalization coming...

Standing. Johan Land filed the claim on the site's proof-claims tab on 5 September 2026, naming the AI systems GPT-6-Astra, Fable 5.1 and Gemini-3.8-Flash, which the tab entry says worked inside a Lean repository built for proof search; the manuscript's AI-provenance line names GPT-6-Astra, Fable 5.1 and Gemini 3.8 (the tab entry writes the third as Gemini-3.8-Flash). The manuscript is posted only in the author's repository and says that it is not peer reviewed. The site's label is OPEN and its page carries no comment; no refereed publication, no site acceptance and no outside review was found (site and thread accessed 2026-10-06). The claim stays claimed.

Lean. The claimant's one comment on the tab, of 6 September 2026, points to the repository linked above as a formalization that compiles with no sorry and no axioms beyond propext, Classical.choice and Quot.sound. The repository's README names the terminal theorem Erdos1059.infinitelyManyFactorialAvoidingPrimes, that the set of primes $p$ with $p-k!$ composite for every $k!<p$ is infinite, reports the same three axioms from its build, uses the toolchain leanprover/lean4:v4.34.0-rc2, and says that no independent replication or external audit is recorded and that no human audit of the correspondence between the Lean statements and the manuscript is recorded. This corpus has not built or audited the development, so no formalized evidence is listed.

Depends on. Nothing on the wiki; the manuscript's outside inputs are the OpenAI long-gaps construction and Vaughan's theorem, named above.