Number theory

Green7.green_7.variants.positive_density

Does Ulam's sequence have positive density?

References

Ben Green's Open Problem 7
erdosproblems.com/342

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → (Set.range a).upperDensity > 0

What you must prove

import FormalConjectures.GreensOpenProblems.«7»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green7.green_7.variants.positive_density" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/7.lean

Source type SHA-256: sha256:6cb80eadee940ba1bcdbcff50243bab3623bb0a40fa74117e1ef6493ae5ee543
Task id: fc-379fc029-variants-positive-density-330bf76f5d-formalized-v1
Task commitment: sha256:be1d37dbae171672a2fe710a7e5b4de4ddd5b41897749e99d308d53ca4e3ccac

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.