Combinatorics

Erdős 120

Let

A \subseteq \mathbb{R}

be an infinite set. Must there be a set

E \subseteq \mathbb{R}

of positive measure which does not contain any set of the shape

a * A + b

for some

a,b \in \mathbb{R}

and

a \neq 0

References

erdosproblems.com/120

St20 Steinhaus, Hugo, Sur les distances des points dans les ensembles de measure positive. Fund. Math. (1920), 93-104.

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

What you must prove

import FormalConjectures.ErdosProblems.«120»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos120.erdos_120" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/120.lean

Source type SHA-256: sha256:0f79ced60a2e616896659f25e6fc019585f8273880dfc18867972dee5510a24b
Task id: fc-379fc029-erdos120-erdos-120-4c0d2e2e09-formalized-v1
Task commitment: sha256:8e22f98271c26ef43ee015d14a5ed983f7922833dc793a58a991e2fd77672295

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.