{"id":"palomar/PALOMAR-2026-09-20-000002","url":"https://github.com/linrock/math-proofs/tree/54f272582dd71321ab9d458663d675edd3d0a463/erdos-689","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-20-000002-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.NT","math.CO","number-theory","covering-problems","lean","erdos-problems"],"score":0,"title":"Erdős 689: eventual double covering by prime residue classes","trust":"high","domain":"math.NT","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.NT","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-20","reactions":{},"formalized":true,"formalizes":[{"title":"A greedy matching proof of Erdős’s two-fold residue-class problem (working manuscript, 27 April 2026)","identifier":"https://www.ulam.ai/research/erdos689.pdf","relationship":"formalizes"}]}