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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/421.lean

Formal Conjectures

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

Continue