Skip to content

Erdős problem 458

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

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

458.lean

Retained formal statement1 of 1

Let lcm⁡(1,…,n)\operatorname{lcm}(1, \dots, n) denote the least common multiple of {1,…,n}\{1, \dots, n\}. Let pkp_k be the kk-th prime. Is it true that for all k≥1k \geq 1, lcm⁡(1,…,pk+1−1)<pk⋅lcm⁡(1,…,pk)\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
True ↔ ∀ (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

Search problems.science

Find a Problem, Result, source, or page