# The geometric case of the Erdős similarity conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The dyadic case of the Erdős similarity conjecture](../../preprints/The-dyadic-case-of-the-Erdos-similarity-conjecture-September-25-2026/paper.pdf)

## Scope

The formalization proves the dyadic case of the Erdős similarity conjecture. For every $0<\eta<1$, it constructs a compact set $E\subset[0,1]$ of measure greater than $1-\eta$ that contains no affine copy of $\{2^{-n}:n\ge1\}$. Explicitly, for every translation $x$ and every nonzero real dilation $s$, some point $x+s2^{-n}$ lies outside $E$. Both signs of $s$ are included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Positive-measure avoidance of every affine dyadic sequence | [DyadicAvoidance.lean](../ComparatorChallenges/DyadicAvoidance.lean) |