---

Claim. Theorem 1.1 of P. Chojecki, A greedy matching proof of Erdős's two-fold residue-class problem, working manuscript dated 27 April 2026, 10 pp., hosted on the author's research site, states that for all sufficiently large $n$ one can choose a residue class for every prime $p\le n$ so that every integer in $[1,n]$ lies in at least two of the classes, the statement of Problem 689. Section 1 names three inputs: the prime number theorem in fixed progressions, the Green--Tao theorem for the ternary system $q,q',bq'-aq$ in primes (the manuscript's Lemma 1.3), and a Selberg upper-bound sieve for two linear forms (its Lemma 1.4); the argument then builds the cover greedily, pairing leftover integers through prime differences. Read depth: the title page and Section 1; Sections 2--5 are not checked here.

Submission note. Posted to the site's forum by Przemek Chojecki on 30 April 2026:

I've done many back-and-forths with GPT-5.5 Pro on this problem and basically the solution converges to some variant of use Green-Tao-Ziegler + hypergraphs, which seems similar to what Malek posted below as well.

The problem is some computations are pretty delicate, so I'm posting this note more as a working manuscript and would love to get experts' opinions on this one.

The Palomar registry's description of entry PALOMAR-2026-09-20-000002:

A complete Lean 4 proof of Erdős problem 689: for all sufficiently large n, one residue class per prime p ≤ n can cover every integer from 1 through n at least twice. The proof follows the argument for Theorem 1.1 in Chojecki’s April 2026 manuscript “A greedy matching proof of Erdős’s two-fold residue-class problem.” The formalization directly proves the required three-prime counting estimate using Fourier analysis, replacing the manuscript’s invocation of Green–Tao, and verifies the sieve bounds and greedy-matching construction in Lean.

Posting. The author posted the manuscript to the site's thread on 30 April 2026, saying that repeated exchanges with an AI system, GPT-5.5 Pro as the post names it, had converged on a variant of the linear-equations-in-primes and hypergraph route, like the notes Zribi had posted days earlier (Zribi's claim page), that some of the computations are delicate, and that the note was offered as a working manuscript for experts' opinions. The argument was later merged with Zribi's notes into the joint submission on the proof-claim tab (21 July 2026).

Formalization. A Lean 4 development by Linmiao Xu in the folder erdos-689 of the public repository linrock/math-proofs (MIT license), linked above at its commit of 20 September 2026, proves the theorem Erdos689.Palomar.eventual_double_cover, the problem's statement for all large $n$, and declares itself a formalization of this manuscript: the abstract of its registry entry says that the proof follows the argument for Theorem 1.1, proves the needed three-prime counting estimate directly by Fourier analysis in place of the Green--Tao input, and verifies the sieve bounds and the greedy matching construction in Lean. The entry also records Fourier, minor-arc, prime-power and arithmetic lemmas ported from another public Lean project at a pinned commit, and a challenge statement that restates the covering proposition of the formal-conjectures declaration erdos_689 without importing it. The Palomar registry replays a submitted proof in the Lean kernel and compares it with a challenge statement; its entry PALOMAR-2026-09-20-000002 (registered 2026-09-20T01:54Z; the two record links above; as of 2026-10-07) records Lean v4.33.1, the Mathlib revision it pins, the permitted axioms propext, Quot.sound and Classical.choice, a 28-line challenge file importing only Mathlib, a kernel verification on 2026-09-20T01:25Z, and an automated review by a language model with a neutral outcome and no warnings; the registry's own description says that it certifies neither novelty nor the match between the formal statement and the informal problem and is not peer review. The development was neither built, replayed nor audited in this corpus, and no statement-fidelity review of its challenge file exists here, so it gives no formalized evidence. The site's page and proof-claim tab do not mention the registration, and the community database recorded the problem open with no formal proof on 2026-10-05.

Standing. Claimed. The site's label is OPEN (page last edited 8 April 2026; thread and proof-claim tab as of 2026-10-07); the maintainer's pinned comment of 2 June 2026 defers any change of label to a refereed publication or an expert's careful reading. No refereed or arXiv version, independent review or site acceptance was found on 2026-10-07.

Depends on. No page of this wiki.