---

Price, working with GPT-5.4 Pro, answers Problem 1202 in the negative. The question asks, for fixed $\epsilon,\eta>0$, whether some $k$ makes every choice of $k$ primes $p_1<\cdots<p_k<n^{1-\epsilon}$, each with a forbidden set $A_i$ of $(p_i-1)/2$ classes modulo $p_i$, leave at most $\epsilon n$ integers $m\leq n$ outside every $A_i$. The construction shows that no $k$ works. In the quantitative form the linked Lean file proves, for every $k$ there are $n$, primes $p_1<\cdots<p_k<n^{9/10}$ and sets $A_i$ of $(p_i-1)/2$ classes each such that more than $n/10$ integers in $[1,n]$ survive, so the statement fails at $\epsilon=1/10$ for every $\eta$; the exponent $9/10$ and the bound $n/10$ are the file's choices, not a form the manuscript is held to state. The primes are taken from one short interval and each $A_i$ is an interval of residues, aligned so that a striped set of positive density avoids every forbidden class; the surviving set contains a long arithmetic progression. The site's commentary reports the construction in quantitative form: for any $c>0$ and $m>\sqrt{n\log n}$ it gives $k\gg_c m^2/(n\log n)$ primes in $(m,2m]$ with half their classes forbidden and at least $(1/2-c)n$ survivors up to $n$, so half the classes modulo $k$ primes of size $O_k(\sqrt{n\log n})$ can be sifted while a positive proportion of $[1,n]$ remains. That form is recorded as the site states it and was not checked. The large sieve gives the affirmative answer when $p_k<n^{1/2}$, so the counterexample lives in the range between $n^{1/2}$ and $n^{1-\epsilon}$ that Erdős asked about.

The manuscript is a read link on an online editor that exposes only the editor's shell and no document (as of 2026-10-07), and no other copy of it is recorded; its argument is known to the corpus only through the external Lean file below, which names a tex/1202.tex that the repository does not carry. The site's revision history (erdosproblems.com/history/1202, accessed 2026-10-07) shows the curator's revisions of 7, 8 and 12 April 2026 each crediting the negative resolution to Liam Price and GPT-5.4 Pro; the current version, last edited 12 April 2026, gives only the surname, and the Lean file's header names Lisa Price, which disagrees. Price is the claimant, with the system named as the site names it.

Reviewed. The site's curator, Thomas Bloom, marks Problem 1202 solved and credits the negative resolution to Price and GPT-5.4 Pro in the site's commentary (last edited 12 April 2026), the reviewed evidence. The manuscript carries no date the corpus can read; the page is dated 7 April 2026, the curator's earliest revision carrying the credit in the site's revision history. No journal publication is recorded, so no refereed evidence is listed.

Formalization. The external file Erdos1202.lean in Boris Alexeev's lean-proofs repository, added on 17 August 2026 and pinned at its commit of 31 August 2026, declares itself a formalization of the interval construction of Price and GPT-5.4 Pro, with Codex and GPT-5.6 Sol as formal authors, so it is a link on this page and not a claim of its own. It states the problem as Erdos1202Statement, quantifying $\epsilon$ and $\eta$ as the site does and bounding by $\epsilon n$, proves erdos_1202_counterexample for every $k$ at exponent $9/10$ and survivor bound $n/10$, and derives not_erdos_1202, the negation of the statement; its prime-counting input is a prime number theorem imported from another Lean project. The file was not built or audited by this corpus, so the claim lists no formalized evidence; the problem page's Current assessment records its read depth.

Depends on. Nothing beyond the cited manuscript.