The site labels the problem PROVED (LEAN) (page last edited 20 January 2026). Müller ([Mu11], refereed) shows that the integers whose odd part is $3\pmod4$ have density $1/2$ and no two of them, equal or not, sum to a power of two, and that no set with the property has lower density above $1/2$; the site's curator, Thomas Bloom, records this as the resolution. The claim page Müller 2011 records the acceptance. The site's (LEAN) suffix is its catalog label; the outside Lean files it rests on are described under Formalization and on the claim pages from their text alone, not built here.