Skip to content

Erdős problem 421

Is there a sequence 1≤d1<d2<…1 \le d_1 < d_2 < \dots with density 1 such that all products ∏u≤i≤vdi\prod_{u \le i \le v} d_i are distinct?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

421.lean

Retained formal statement1 of 1

Is there a sequence 1≤d1<d2<…1 \le d_1 < d_2 < \dots with density 1 such that all products ∏u≤i≤vdi\prod_{u \le i \le v} d_i are distinct?

FormalConjectures/ErdosProblems/421.leanErdos421.erdos_42110 linesExact file
True ↔  ∃ d,    StrictMono d ∧      1 ≤ d 0 ∧        (Set.range d).HasDensity 1 ∧          Set.InjOn            (fun x =>              match x with              | (u, v) => ∏ i ∈ Finset.Icc u v, d i)            {(u, v) | u ≤ v}
OpenStatement only, no proof