{"id":"palomar/PALOMAR-2026-10-16-000022","url":"https://github.com/AItoBit/erdos-656-lean/tree/5f2ab8de0634f343917b0d122153640f293b0e20","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000022-v1.json","repo":"https://github.com/AItoBit/erdos-656-lean","tags":["math.DS","math.CO","msc:37A44","msc:11B13","msc:68V15","additive-combinatorics","erdos-problems","lean-formalization","ergodic-theory"],"score":0,"title":"Erdős Problem 656: translated restricted pair sums","trust":"high","domain":"math.DS","source":"palomar","authors":["AItoBit"],"reviews":0,"subject":"math.DS","summary":"A reproduction of a complete Lean proof that every set A of natural numbers with positive ordinary upper asymptotic density contains an infinite subset B whose distinct pair sums, after one integer translation, all lie in A. This is the exact ordinary-density statement of Erdős Problem 656, an instance of Kra–Moreira–Richter–Robertson Theorem 1.2(i).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"A proof of Erdős's B+B+t conjecture","identifier":"doi:10.1090/cams/34","relationship":"formalizes"},{"title":"Erdős Problem 656","identifier":"","relationship":"formalizes"}]}