Erdős Problem 427

Reference: erdosproblems.com/427

def Erdos427 : Prop

The predicate that for every $n$ and $d$, there exists $k$ such that $$ d \mid p_{n + 1} + \cdots + p_{n + k}, $$ where $p_r$ denotes the $r$th prime?

Equations

• Erdos427 = ∀ (n d : ℕ), d ≠ 0 → ∃ (k : ℕ), k ≠ 0 ∧ d ∣ ∑ i ∈ Finset.Ico n (n + k), Nat.nth Nat.Prime i

theorem erdos_427 : Erdos427 ↔ True

Erdős Problem 427: is it true that, for every $n$ and $d$, there exists $k$ such that $$ d \mid p_{n + 1} + \cdots + p_{n + k}, $$ where $p_r$ denotes the $r$th prime?

def ShiuTheorem : Prop

The statement of Shiu's theorem: for any $k \geq 1$ and $(a, q) = 1$ there exist infinitely many $k$-tuples of consecutive primes $p_m, ..., p_{m + k - 1}$ all of which are congruent to $a$ modulo $q$.

[Sh00] Shiu, D. K. L., Strings of congruent primes. J. London Math. Soc. (2) (2000), 359-373.

Equations

• ShiuTheorem = ∀ (k a q : ℕ), 1 ≤ k → 1 ≤ q → a.gcd q = 1 → {m : ℕ | ∀ p ∈ Finset.image (Nat.nth Nat.Prime) (Finset.Ico m (m + k)), p ≡ a [MOD q]}.Infinite

theorem erdos_427.shiu : ShiuTheorem

Shiu's theorem: for any $k \geq 1$ and $(a, q) = 1$ there exist infinitely many $k$-tuples of consecutive primes $p_m, ..., p_{m + k - 1}$ all of which are congruent to $a$ modulo $q$.

[Sh00] Shiu, D. K. L., Strings of congruent primes. J. London Math. Soc. (2) (2000), 359-373.

theorem erdos_427.of_shiu (H : ShiuTheorem) : Erdos427

Cedric Pilatte has observed that a positive solution to Erdős Problem 427 follows from Shiu's theorem.