Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. For every nondecreasing unbounded f:N→Z≥0f:\mathbb N\to\mathbb Z_{\ge0} there is an admissible set A⊆NA\subseteq\mathbb N (one that misses at least one residue class modulo every prime) with ∣A∩{1,…,N}∣≤f(N)|A\cap\{1,\ldots,N\}|\le f(N) for all NN such that A+nA+n is not contained in the primes for any n∈Zn\in\mathbb Z. So no sparsity threshold of the kind Problem 429 asks for exists, and the answer to the question is no. This is Theorem 1 of D. Weisenberg, Sparse admissible sets and a problem of Erdős and Graham, Integers 24 (2024), Article A89 (result page Theorem 1; source card Weisenberg 2024), which states the conjecture it refutes as its Conjecture 1 and names the problem's number. The theorem builds AA inside the powers of an integer aa that is a primitive root modulo infinitely many primes, two members in each nonzero class modulo each such prime in turn; a shift carrying AA into the primes would be divisible by every one of those primes, hence zero, and AA itself is not a set of primes. Section 2 of the paper gives three further constructions of such sets, the second using only the Chinese remainder theorem. The claim concerns the exact question: it says nothing about the site's squarefree (p2p^2) variant, which the paper does not treat.

Depends on. No page of this wiki. The first construction consumes the existence of a positive integer that is a primitive root modulo infinitely many primes, which the paper cites to Gupta and Ram Murty (Invent. Math. 78 (1984)) and Heath-Brown (Quart. J. Math. Oxford (2) 37 (1986)), neither held; the second construction avoids that input, so the disproof does not rest on it.

Acceptance. Refereed: the paper appeared in Integers, a refereed journal (received 24 June 2024, accepted 20 September 2024, published 9 October 2024, per the article's header; the journal's volume 24 contents page lists Article A89). Not reviewed: the site's curator, Thomas Bloom, labels the problem DISPROVED (LEAN) and credits this paper in the commentary (page last edited 8 April 2026), and the paper reports on p. 2 that the site marked the problem solved when the first construction appeared as a preprint, but its acknowledgement (p. 4) thanks Bloom for reviewing an earlier draft of the paper and for advising the author in the Oxford mathematics master's program, so Bloom is not independent of the claimant and the credit is not reviewed evidence; the community database lists the Lean suffix with a last update of 29 January 2026 on its status entry. No dispute of the construction, second resolution or citing paper was found in the search recorded on the problem page. This project's own reading of the one-paragraph proof, recorded on the source card, is not acceptance evidence.

Formalization. The site's "(Lean)" suffix followed the file posted in the site's discussion thread on 29 January 2026 by the account Woett, whose comment says that Aristotle formalized the paper's second proof; the file's header names Aristotle, the automated prover of Harmonic, and the file is linked above at its last change, of 2 March 2026, a later revision than the one posted. Boris Alexeev's plby/lean-proofs collection holds a later port of the same development for a later toolchain, committed 30 June 2026 and linked above, whose header names Aristotle and Wouter van Doorn as its formal authors and the thread's file as its origin; the formal-conjectures statement file names that port in its formal_proof attribute, and that statement file, whose theorem has a sorry body, is linked above as a record, not as a formalization. Each development declares itself a formalization of this paper's second construction. Both prove a main_theorem producing, for every f→∞f\to\infty, an infinite admissible set with counting function at most ff and, for every integer shift, a member whose shift is not prime. Their statements are compared with the collection's erdos_429 on the problem page; neither has been built or kernel-checked in this corpus and no statement-fidelity review exists, so formalized is not listed as evidence.