Erdős problem 458

Let $\operatorname{lcm}(1, \dots, n)$ denote the least common multiple of $\{1, \dots, n\}$ . Let $p_k$ be the $k$ -th prime. Is it true that for all $k \geq 1$ , $\operatorname{lcm}(1, \dots, p_{k+1}-1) < p_k \cdot \operatorname{lcm}(1, \dots, p_k)$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

458.lean

Retained formal statement1 of 1

Let $\operatorname{lcm}(1, \dots, n)$ denote the least common multiple of $\{1, \dots, n\}$ . Let $p_k$ be the $k$ -th prime. Is it true that for all $k \geq 1$ , $\operatorname{lcm}(1, \dots, p_{k+1}-1) < p_k \cdot \operatorname{lcm}(1, \dots, p_k)$ ?

FormalConjectures/ErdosProblems/458.leanErdos458.erdos_4581 lineExact file

1True ↔ ∀ (k : ℕ), Erdos458.lcm_upto (Nat.nth Prime (k + 1) - 1) < Nat.nth Prime k * Erdos458.lcm_upto (Nat.nth Prime k)

OpenStatement only, no proof