Skip to content

Erdős problem 1056

Start work

Let k≥2k ≥ 2. Does there exist a prime pp and consecutive intervals I0,…,IkI_0,\dots,I_k such that ∏n∈Iin≡1mod  n\prod\limits_{n{\in}I_i}n \equiv 1 \mod n for all 1≤i≤k1 \le i \le k?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1056.lean

Retained formal statement1 of 4

Let k≥2k ≥ 2. Does there exist a prime pp and consecutive intervals I0,…,IkI_0,\dots,I_k such that ∏n∈Iin≡1mod  n\prod\limits_{n{\in}I_i}n \equiv 1 \mod n for all 1≤i≤k1 \le i \le k?

FormalConjectures/ErdosProblems/1056.leanErdos1056.erdos_10563 linesExact file
True ↔  ∀ k ≥ 2,    ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries
OpenStatement only, no proof