Number theory

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)

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«458»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos458.erdos_458" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/458.lean

Source type SHA-256: sha256:909d60f631d5bf196c4bbe998c7ccc755c1f67be8a90e99926311a249344db99
Task id: fc-v2-erdos458-erdos-458-8d22a48ef5b2899a131e121d-formalized
Task commitment: sha256:d7dc22afb490da1579c9f5c592895e10227345e9d3bbc3d1759ac61d69d5186d

References

erdosproblems.com/458

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

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)