Erdős Problem 458

Reference: erdosproblems.com/458

def Erdos458.lcm_upto (n : ℕ) : ℕ

The least common multiple of the integers in the set $\{1, \dots, n\}$.

Equations

• Erdos458.lcm_upto n = (Finset.Icc 1 n).lcm id

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

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)$?