Erdős Problem 1056

Reference: erdosproblems.com/1056

def Erdos1056.AllModProdEqualsOne (p : ℕ) {k : ℕ} (boundaries : Fin (k + 1) → ℕ) : Prop

The proposition that the modular product of a collection of consecutive interval equals $1$ modulo $p$, where intervals are defined by a function specifying the consecutive boundaries.

Equations

• Erdos1056.AllModProdEqualsOne p boundaries = ∀ (i : Fin k), ∏ n ∈ Finset.Ico (boundaries i.castSucc) (boundaries (i.castSucc + 1)), n ≡ 1 [MOD p]

theorem Erdos1056.erdos_1056 : (∀ k ≥ 2, ∃ (p : ℕ) (_ : Nat.Prime p) (boundaries : Fin (k + 1) → ℕ) (_ : StrictMono boundaries), AllModProdEqualsOne p boundaries) ↔ sorry

Let $k ≥ 2$. Does there exist a prime $p$ and consecutive intervals $I_0,\dots,I_k$ such that $\prod\limits_{n{\in}I_i}n \equiv 1 \mod n$ for all $1 \le i \le k$?

theorem Erdos1056.erdos_1056_k2 : AllModProdEqualsOne 11 ![3, 5, 8]

This is problem A15 in Guy's collection [Gu04], where he reports that in a letter in 1979 Erdős observed that $3 * 4 \equiv 5 * 6 * 7 \equiv 1 \mod 11$.

theorem Erdos1056.erdos_1056_k3 : AllModProdEqualsOne 17 ![2, 6, 12, 16]

Makowski [Ma83] found, for $k=3$: $2 * 3 * 4 * 5 \equiv 6 * 7 * 8 * 9 * 10 * 11 \equiv 12 * 13 * 14 * 15 \equiv 1 \mod 17$.

theorem Erdos1056.noll_simmons : (∀ᶠ (k : ℕ) in Filter.atTop, ∃ (p : ℕ) (_ : Nat.Prime p) (Q : Fin k → ℕ) (_ : StrictMono Q) (_ : ∀ (i : Fin k), Q i < p), ∀ (i j : Fin k), (Q i).factorial ≡ (Q j).factorial [MOD p]) ↔ sorry

Noll and Simmons asked, more generally, whether there are solutions to $q_1! \equiv \dots \equiv q_k! \mod p$ for arbitrarily large $k$ (with $q_1 < \dots < q_k$).