Erdős problem 421 · problems.science

Is there a sequence $1 \le d_1 < d_2 < \dots$ with density 1 such that all products $\prod_{u \le i \le v} d_i$ are distinct?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

421.lean

Retained formal statement1 of 1

Is there a sequence $1 \le d_1 < d_2 < \dots$ with density 1 such that all products $\prod_{u \le i \le v} d_i$ are distinct?

FormalConjectures/ErdosProblems/421.leanErdos421.erdos_42110 linesExact file

1True ↔2  ∃ d,3    StrictMono d ∧4      1 ≤ d 0 ∧5        (Set.range d).HasDensity 1 ∧6          Set.InjOn7            (fun x =>8              match x with9              | (u, v) => ∏ i ∈ Finset.Icc u v, d i)10            {(u, v) | u ≤ v}

OpenStatement only, no proof

Sources

Search problems.science