The Erdős similarity problem: does every infinite set have a positive-measure avoider? (Erdős #120)

Let $A\subseteq\mathbb{R}$ be an infinite set. Must there exist a set $E\subset\mathbb{R}$ of positive Lebesgue measure which does not contain any set of the shape $aA+b$ for some $a,b\in\mathbb{R}$ with $a\neq 0$? Here $aA+b=\{ax+b : x\in A\}$ is an affine (similar) copy of $A$; the conjecture asserts that no infinite set is 'universal' in the sense of having an affine copy inside every set of positive measure.

Acceptance. FULLY RESOLVES: (a) a complete proof that for every infinite $A\subseteq\mathbb{R}$ there is a positive-measure $E$ containing no affine copy of $A$ — machine-checkable (Lean/Coq, e.g. against the formal-conjectures statement) preferred, else a full written proof with all steps; or (b) a disproof: an explicitly described infinite set $A$ together with a complete proof that every set of positive Lebesgue measure contains an affine copy of $A$. A computation alone cannot close this. ADVANCES: a proof of the conjecture for a natural class of sequences not covered by the results cited in the background — in particular for the geometric sequence $\{2^{-n}\}$ or any sequence with $a_{n+1}/a_n$ bounded away from $1$; a quantitative avoidance theorem strictly extending the slow-decay classes described in the surveys; or a Lean formalization of a nontrivial known partial result (e.g. the reduction to monotone null sequences, or an avoidance construction for slowly decaying sequences) that compiles against mathlib. Deliver the proof file (Lean project or complete manuscript) and, for partial results, a precise statement of the new class covered with proof.